open import Category -- https://github.com/konn/category-agda
open import Level

module discrete where

open import Relation.Binary.Core

data  TwoObject {c₁ : Level}  : Set c₁ where
   t0 : TwoObject
   t1 : TwoObject

---
---  two objects category  ( for limit to equalizer proof )
---
---          f
---       -----→
---     0         1
---       -----→
---          g
--
--     missing arrows are constrainted by TwoHom data

data TwoHom {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
   id-t0 : TwoHom t0 t0
   id-t1 : TwoHom t1 t1
   arrow-f :  TwoHom t0 t1
   arrow-g :  TwoHom t0 t1


comp :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f   =   arrow-f 
comp {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  =   arrow-g 
comp {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    =   id-t1 
comp {_}  {_}  {t0} {t0} {t1}  arrow-f   id-t0    =   arrow-f 
comp {_}  {_}  {t0} {t0} {t1}  arrow-g   id-t0    =   arrow-g 
comp {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    =   id-t0 

open TwoHom

_×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  ( TwoHom {c₁}  {c₂} b c ) →  ( TwoHom {c₁} {c₂} a b )  →  ( TwoHom {c₁}  {c₂} a c )
_×_  {c₁}  {c₂}  {a} {b} {c} f g  =  comp  {c₁}  {c₂}  {a} {b} {c} f g


--          f    g    h
--       d <- c <- b <- a
--
--   It can be proved without TwoHom constraints

assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
       {f : (TwoHom {c₁}  {c₂ } c d )} →
       {g : (TwoHom {c₁}  {c₂ } b c )} →
       {h : (TwoHom {c₁}  {c₂ } a b )} →
       ( f × (g × h)) ≡ ((f × g) × h )
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0  } = refl
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0  } = refl
assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0  } = refl
assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0  } = refl
assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0  } = refl
assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1  } = refl

TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
TwoId {_} {_} t0 = id-t0 
TwoId {_} {_} t1 = id-t1 

open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )

TwoCat : {c₁ c₂ : Level  } →  Category   c₁  c₂  c₂
TwoCat   {c₁}  {c₂} = record {
    Obj  = TwoObject  {c₁} ;
    Hom = λ a b →    ( TwoHom {c₁}  {c₂ } a b ) ;
    _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
    _≈_ =  λ x y → x  ≡ y ;
    Id  =  λ{a} → TwoId {c₁ } { c₂} a ;
    isCategory  = record {
            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
            identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
            identityR  = λ{a b f} → identityR {c₁}  {c₂ } {a} {b} {f} ;
            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
            associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
       }
   }  where
        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  ≡ f
        identityL  {c₁}  {c₂}  {t1} {t1} { id-t1 } = refl
        identityL  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  ≡ f
        identityR  {c₁}  {c₂}  {t1} {t1} { id-t1  } = refl
        identityR  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
            f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  = 
          let open  ≡-Reasoning in begin
                    ( h × f )
                ≡⟨ refl ⟩
                    comp (h) (f)
                ≡⟨ cong (λ x  → comp ( h ) x )  f==g ⟩
                    comp (h) (g)
                ≡⟨ cong (λ x  → comp x ( g ) )  h==i ⟩
                    comp (i) (g)
                ≡⟨ refl ⟩
                    ( i × g )
                ∎