open import Category -- https://github.com/konn/category-agda open import Level module discrete where open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) module graphtocat where data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where id : ( a : obj ) → Arrow a a mono : { a b : obj } → hom a b → Arrow a b connected : {a b : obj } → {c : obj} → hom b c → Arrow {obj} {hom} a b → Arrow a c _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c id a + id .a = id a id b + mono x = mono x id a + connected x y = connected x y mono x + id a = mono x mono x + mono y = connected x (mono y) mono x + connected y z = connected x ( connected y z ) connected x y + z = connected x ( y + z ) assoc-+ : { obj : Set } { hom : obj → obj → Set } {a b c d : obj } (f : (Arrow {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) → ( f + (g + h)) ≡ ((f + g) + h ) assoc-+ (id a) (id .a) (id .a) = refl assoc-+ (id a) (id .a) (mono x) = refl assoc-+ (id a) (id .a) (connected h h₁) = refl assoc-+ (id a) (mono x) (id a₁) = refl assoc-+ (id a) (mono x) (mono x₁) = refl assoc-+ (id a) (mono x) (connected h h₁) = refl assoc-+ (id a) (connected g h) _ = refl assoc-+ (mono x) (id a) (id .a) = refl assoc-+ (mono x) (id a) (mono x₁) = refl assoc-+ (mono x) (id a) (connected h h₁) = refl assoc-+ (mono x) (mono x₁) (id a) = refl assoc-+ (mono x) (mono x₁) (mono x₂) = refl assoc-+ (mono x) (mono x₁) (connected h h₁) = refl assoc-+ (mono x) (connected g g₁) _ = refl assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y ) open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) → Category Level.zero Level.zero Level.zero GraphtoCat obj hom = record { Obj = obj ; Hom = λ a b → Arrow a b ; _o_ = λ{a} {b} {c} x y → _+_ x y ; _≈_ = λ x y → x ≡ y ; Id = λ{a} → id a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ; identityR = λ{a b f} → identityR {a} {b} {f} ; o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = λ{a b c d f g h } → assoc-+ f g h } } where identityL : {A B : obj } {f : ( Arrow A B) } → ((id B) + f) ≡ f identityL {_} {_} {id a} = refl identityL {_} {_} {mono x} = refl identityL {_} {_} {connected x f} = refl identityR : {A B : obj } {f : ( Arrow {obj} {hom} A B) } → ( f + id A ) ≡ f identityR {_} {_} {id a} = refl identityR {_} {_} {mono x} = refl identityR {_} {_} {connected x f} = cong (λ k → connected x k) ( identityR {_} {_} {f} ) o-resp-≈ : {A B C : obj } {f g : ( Arrow A B)} {h i : ( Arrow B C)} → f ≡ g → h ≡ i → ( h + f ) ≡ ( i + g ) o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl data TwoObject : Set 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 : TwoObject → TwoObject → Set where id-t0 : TwoHom t0 t0 id-t1 : TwoHom t1 t1 arrow-f : TwoHom t0 t1 arrow-g : TwoHom t0 t1 TwoCat' : Category Level.zero Level.zero Level.zero TwoCat' = GraphtoCat TwoObject TwoHom where open graphtocat _×_ : {a b c : TwoObject } → TwoHom b c → TwoHom a b → TwoHom a c _×_ {t0} {t1} {t1} id-t1 arrow-f = arrow-f _×_ {t0} {t1} {t1} id-t1 arrow-g = arrow-g _×_ {t1} {t1} {t1} id-t1 id-t1 = id-t1 _×_ {t0} {t0} {t1} arrow-f id-t0 = arrow-f _×_ {t0} {t0} {t1} arrow-g id-t0 = arrow-g _×_ {t0} {t0} {t0} id-t0 id-t0 = id-t0 open TwoHom -- f g h -- d <- c <- b <- a -- -- It can be proved without TwoHom constraints assoc-× : {a b c d : TwoObject } {f : (TwoHom c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} → ( f × (g × h)) ≡ ((f × g) × h ) assoc-× {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl assoc-× {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl assoc-× {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl assoc-× {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl assoc-× {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl assoc-× {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl TwoId : (a : TwoObject ) → (TwoHom a a ) TwoId t0 = id-t0 TwoId t1 = id-t1 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) TwoCat : Category Level.zero Level.zero Level.zero TwoCat = record { Obj = TwoObject ; Hom = λ a b → TwoHom a b ; _≈_ = λ x y → x ≡ y ; Id = λ{a} → TwoId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ; identityR = λ{a b f} → identityR {a} {b} {f} ; o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = λ{a b c d f g h } → assoc-× {a} {b} {c} {d} {f} {g} {h} } } where identityL : {A B : TwoObject } {f : ( TwoHom A B) } → ((TwoId B) × f) ≡ f identityL {t1} {t1} { id-t1 } = refl identityL {t0} {t0} { id-t0 } = refl identityL {t0} {t1} { arrow-f } = refl identityL {t0} {t1} { arrow-g } = refl identityR : {A B : TwoObject } {f : ( TwoHom A B) } → ( f × TwoId A ) ≡ f identityR {t1} {t1} { id-t1 } = refl identityR {t0} {t0} { id-t0 } = refl identityR {t0} {t1} { arrow-f } = refl identityR {t0} {t1} { arrow-g } = refl o-resp-≈ : {A B C : TwoObject } {f g : ( TwoHom A B)} {h i : ( TwoHom B C)} → f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {a} {b} {c} {f} {.f} {h} {.h} refl refl = refl -- Category with no arrow but identity open import Data.Empty DiscreteCat' : (S : Set) → Category Level.zero Level.zero Level.zero DiscreteCat' S = GraphtoCat S ( λ _ _ → ⊥ ) where open graphtocat record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) : Set c₁ where field discrete : a ≡ b -- if f : a → b then a ≡ b dom : S dom = a open DiscreteHom _*_ : ∀ {c₁} → {S : Set c₁} {a b c : S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) } DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) → DiscreteHom {c₁} a a DiscreteId a = record { discrete = refl } open import Relation.Binary.PropositionalEquality assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : S} {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → dom ( f * (g * h)) ≡ dom ((f * g) * h ) assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁ DiscreteCat {c₁} S = record { Obj = S ; Hom = λ a b → DiscreteHom {c₁} {S} a b ; _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be Id = λ{a} → DiscreteId a ; isCategory = record { isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; identityL = λ{a b f} → identityL {a} {b} {f} ; identityR = λ{a b f} → identityR {a} {b} {f} ; o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h} } } where identityL : {a b : S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f identityL {a} {b} {f} = refl identityR : {A B : S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f identityR {a} {b} {f} = refl o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g ) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl