{-# OPTIONS --without-K #-}
module Composition.Horizontal where

open import Level
open import Type hiding ()
open import Function
open import Relation.Binary

Arrow :  {i}   i   j   (suc j  i)
Arrow = Rel

HComposition :  {a } {A :  a}  Arrow A    _
HComposition = Transitive

Identity :  {a } {A :  a}  Arrow A    _
Identity = Reflexive

IArrow :  {i j t} {I :  i} (_↝ᵢ_ : Arrow I j) (T : I   t) a   _
IArrow _↝ᵢ_ T a =  {i₀ i₁}  i₀ ↝ᵢ i₁  T i₀  T i₁   a

IReflexivity :  {a i j t} {I :  i} {R : Rel I j} {T : I   t}  Reflexive R  IArrow R T a   _
IReflexivity R-refl Arr =  {i A}  Arr (R-refl {i}) A A

IIdentity :  {a i j t} {I :  i} {_↝ᵢ_ : Arrow I j} {T : I   t}  Identity _↝ᵢ_  IArrow _↝ᵢ_ T a   _
IIdentity = IReflexivity

ITrans :  {i j t a} {I :  i}
           {R₀ R₁ R₂ : Rel I j}
           {T : I   t}
           (R-trans : Trans R₀ R₁ R₂)
           (Arr₀ : IArrow R₀ T a)
           (Arr₀ : IArrow R₁ T a)
           (Arr₀ : IArrow R₂ T a)
           _
ITrans R-trans Arr₀ Arr₁ Arr₂
  =  {i₀ i₁ i₂ j₀ j₁}  Trans (Arr₀ j₀) (Arr₁ j₁)
                           (Arr₂ (R-trans {i₀} {i₁} {i₂} j₀ j₁))

ITransitive :  {i j t a} {I :  i} {R : Rel I j}
                {T : I   t}
               Transitive R  IArrow R T a   _
ITransitive {R = R} R-trans Arr
  = ITrans {R₀ = R} R-trans Arr Arr Arr

IHComposition :  {i j t a} {I :  i}
                 {_↝ᵢ_ : Arrow I j} {T : I   t}
                 (_·_ : HComposition _↝ᵢ_)
                 (⟨_⟩_↝_ : IArrow _↝ᵢ_ T a)   _
IHComposition = ITransitive

record IHComposable {i j t a} {I :  i}
                    {_↝ᵢ_ : Arrow I j} {T : I   t}
                    (_·_ : HComposition _↝ᵢ_)
                    (⟨_⟩_↝_ : IArrow _↝ᵢ_ T a)
                  :  (a  t  i  j) where
  constructor mk
  infixr 1 _>>>_
  field
    _>>>_ : IHComposition  {η}  _·_ {η}) ⟨_⟩_↝_

open import Relation.Binary.PropositionalEquality
Refl-Unit :  { a} {A :  a} {R : Rel A }  Reflexive R  Transitive R   _
Refl-Unit {R = R} R-refl R-trans =  {x y} (p : R x y)  R-trans R-refl p  p

open import Data.One using (𝟙)
ConstArr :  {a} (A :  a)  𝟙  𝟙   a
ConstArr A _ _ = A

HComposable :  {t a} {T :  t} (_↝_ : T  T   a)   (t  a)
HComposable _↝_ = IHComposable {i = zero} {_↝ᵢ_ = ConstArr 𝟙} _ (const _↝_)

{- Composable, unfolded:
record HComposable {t a} {T : ★ t} (_↝_ : T → T → ★ a) : ★ (t ⊔ a) where
  constructor mk
  infixr 1 _>>>_
  field
    _>>>_ : ∀ {A B C} → (A ↝ B) → (B ↝ C) → (A ↝ C)
-}

constHComp' :  {a} {A :  a} (_·_ : A  A  A)  HComposition (ConstArr A)
constHComp' _·_ = _·_

constHComp :  {a} {A :  a} (_·_ : A  A  A)  HComposable (ConstArr A)
constHComp _·_ = mk _·_

module HComposable = IHComposable

ixFunHComp :  {ix t} {Ix :  ix} (F : Ix   t)  HComposable  i o  F i  F o)
ixFunHComp _ = mk  f g x  g (f x))

funHComp :  {t}  HComposable  (A B :  t)  A  B)
funHComp = ixFunHComp id

opHComp :  {t a} {T :  t} {_↝_ : T  T   a}  HComposable _↝_  HComposable (flip _↝_)
opHComp (mk _>>>_) = mk (flip _>>>_)

module _ {a} (A :  a) where
    open import Data.Vec.NP
    open FunVec {A = A}
    vecFunHComp : HComposable _→ᵛ_
    vecFunHComp = ixFunHComp (Vec A)

open import Data.Bits
bitsFunHComp : HComposable _→ᵇ_
bitsFunHComp = ixFunHComp Bits