Mercurial > hg > Members > kono > Proof > category
view limit-to.agda @ 426:1290d6876129
Functor MA → A
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 26 Mar 2016 10:16:05 +0900 |
| parents | 98811e927d4a |
| children | 531b739a1d7c |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level module limit-to where open import cat-utility open import HomReasoning open import Relation.Binary.Core open import Data.Maybe open Functor -- If we have limit then we have equalizer --- two objects category --- --- f --- ------> --- 0 1 --- ------> --- g data TwoObject {c₁ : Level} : Set c₁ where t0 : TwoObject t1 : TwoObject -- constrainted arrow -- we need inverse of f to complete cases data Arrow {c₁ c₂ : Level } ( t00 t11 : TwoObject {c₁} ) : TwoObject {c₁} -> TwoObject {c₁} -> Set c₂ where id-t0 : Arrow t00 t11 t00 t00 id-t1 : Arrow t00 t11 t11 t11 arrow-f : Arrow t00 t11 t00 t11 arrow-g : Arrow t00 t11 t00 t11 inv-f : Arrow t00 t11 t11 t00 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set c₂ where field hom : Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) open TwoHom -- arrow composition comp : ∀ {c₁ c₂} -> {a b c : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 b c ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a c ) comp {_} {_} {_} {_} {_} nothing _ = nothing comp {_} {_} {_} {_} {_} (just _ ) nothing = nothing comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-f ) = just arrow-f comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-g ) = just arrow-g comp {_} {_} {t1} {t1} {t1} (just id-t1 ) ( just id-t1 ) = just id-t1 comp {_} {_} {t1} {t1} {t0} (just inv-f ) ( just id-t1 ) = just inv-f comp {_} {_} {t0} {t0} {t1} (just arrow-f ) ( just id-t0 ) = just arrow-f comp {_} {_} {t0} {t0} {t1} (just arrow-g ) ( just id-t0 ) = just arrow-g comp {_} {_} {t0} {t0} {t0} (just id-t0 ) ( just id-t0 ) = just id-t0 comp {_} {_} {t1} {t0} {t0} (just id-t0 ) ( just inv-f ) = just inv-f comp {_} {_} {_} {_} {_} (just _ ) ( just _ ) = nothing _×_ : ∀ {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 = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) } _==_ : ∀{ c₁ c₂ a b } -> Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂) _==_ = Eq _≡_ map2hom : ∀{ c₁ c₂ } -> {a b : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) -> TwoHom {c₁} {c₂ } a b map2hom {_} {_} {t1} {t1} (just id-t1) = record { hom = just id-t1 } map2hom {_} {_} {t0} {t1} (just arrow-f) = record { hom = just arrow-f } map2hom {_} {_} {t0} {t1} (just arrow-g) = record { hom = just arrow-g } map2hom {_} {_} {t0} {t0} (just id-t0) = record { hom = just id-t0 } map2hom {_} {_} {_} {_} _ = record { hom = nothing } record TwoHom1 {c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where field Map : TwoHom {c₁} {c₂ } a b iso-Map : Map ≡ map2hom ( hom Map ) open TwoHom1 ==refl : ∀{ c₁ c₂ a b } -> ∀ {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == x ==refl {_} {_} {_} {_} {just x} = just refl ==refl {_} {_} {_} {_} {nothing} = nothing ==sym : ∀{ c₁ c₂ a b } -> ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == y → y == x ==sym (just x≈y) = just (≡-sym x≈y) ==sym nothing = nothing ==trans : ∀{ c₁ c₂ a b } -> ∀ {x y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } → x == y → y == z → x == z ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z) ==trans nothing nothing = nothing ==cong : ∀{ c₁ c₂ a b c d } -> ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → (f : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) -> Maybe (Arrow {c₁} {c₂} t0 t1 c d ) ) -> x == y → f x == f y ==cong { c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl ==cong { c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl) = ==refl module ==-Reasoning {c₁ c₂ : Level} where infixr 2 _∎ infixr 2 _==⟨_⟩_ _==⟨⟩_ infix 1 begin_ data _IsRelatedTo_ {c₁ c₂ : Level} {a b : TwoObject {c₁} } (x y : (Maybe (Arrow {c₁} {c₂} t0 t1 a b ))) : Set c₂ where relTo : (x≈y : x == y ) → x IsRelatedTo y begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x IsRelatedTo y → x == y begin relTo x≈y = x≈y _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } → x == y → y IsRelatedTo z → x IsRelatedTo z _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z) _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x IsRelatedTo y → x IsRelatedTo y _ ==⟨⟩ x≈y = x≈y _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) → x IsRelatedTo x _∎ _ = relTo ==refl -- TwoHom1Eq : {c₁ c₂ : Level } {a b : TwoObject {c₁} } {f g : ( TwoHom1 {c₁} {c₂ } a b)} → -- hom (Map f) == hom (Map g) → f == g -- TwoHom1Eq = ? -- f g h -- d <- c <- b <- a -- -- It can be proved without Arrow 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 )} → hom ( f × (g × h)) == hom ((f × g) × h ) assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | just id-t0 = ==refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | just id-t0 = ==refl assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | just id-t0 = ==refl assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | just id-t0 = ==refl assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | just id-t0 = ==refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-f = ==refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-g = ==refl assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just id-t1 = ==refl -- remaining all failure case (except inf-f case ) assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just _) = nothing assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-f) = nothing assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-g) = nothing assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just inv-f) = ==refl assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just inv-f) = nothing assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just inv-f) = nothing assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just id-t1) = ==refl assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just inv-f) | (just id-t1) = ==refl assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just inv-f) | (just id-t1) = ==refl assoc-× {_} {_} {t1} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just id-t1) = ==refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = record { hom = just id-t0 } TwoId {_} {_} t1 = record { hom = just id-t1 } open import maybeCat -- identityL {c₁} {c₂} {_} {b} {nothing} = let open ==-Reasoning {c₁} {c₂} in -- begin -- (TwoId b × nothing) -- ==⟨ {!!} ⟩ -- nothing -- ∎ open import Relation.Binary 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 -> hom x == hom 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) } → hom ((TwoId B) × f) == hom f identityL {c₁} {c₂} {_} {_} {f} with hom f identityL {c₁} {c₂} {t0} {t0} {_} | nothing = nothing identityL {c₁} {c₂} {t0} {t1} {_} | nothing = nothing identityL {c₁} {c₂} {t1} {t0} {_} | nothing = nothing identityL {c₁} {c₂} {t1} {t1} {_} | nothing = nothing identityL {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl identityL {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl identityL {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) == hom f identityR {c₁} {c₂} {_} {_} {f} with hom f identityR {c₁} {c₂} {t0} {t0} {_} | nothing = nothing identityR {c₁} {c₂} {t0} {t1} {_} | nothing = nothing identityR {c₁} {c₂} {t1} {t0} {_} | nothing = nothing identityR {c₁} {c₂} {t1} {t1} {_} | nothing = nothing identityR {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl identityR {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl identityR {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl identityR {c₁} {c₂} {t0} {t1} {_} | just 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)} → hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = let open ==-Reasoning {c₁} {c₂ } in begin hom ( h × f ) ==⟨⟩ comp (hom h) (hom f) ==⟨ ==cong (\ x -> comp ( hom h ) x ) f==g ⟩ comp (hom h) (hom g) ==⟨ ==cong (\ x -> comp x ( hom g ) ) h==i ⟩ comp (hom i) (hom g) ==⟨⟩ hom ( i × g ) ∎ indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A ) indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { FObj = λ a → fobj a ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { identity = \{x} -> identity {x} ; distr = \ {a} {b} {c} {f} {g} -> distr1 {a} {b} {c} {f} {g} ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f} } } where I = TwoCat {c₁} {c₂} {ℓ} MA = MaybeCat A fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b fmap : {x y : Obj I } -> (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y) fmap {x} {y} h with hom h fmap {t0} {t0} h | just id-t0 = id1 MA a fmap {t1} {t1} h | just id-t1 = id1 MA b fmap {t0} {t1} h | just arrow-f = record { hom = just f } fmap {t0} {t1} h | just arrow-g = record { hom = just g } fmap {_} {_} h | _ = record { hom = nothing } ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → MA [ fmap f ≈ fmap g ] ≈-cong {a} {b} {f1} {g1} f≈g with hom f1 | hom g1 ≈-cong {t0} {t0} {f1} {g1} nothing | nothing | nothing = nothing ≈-cong {t0} {t1} {f1} {g1} nothing | nothing | nothing = nothing ≈-cong {t1} {t0} {f1} {g1} nothing | nothing | nothing = nothing ≈-cong {t1} {t1} {f1} {g1} nothing | nothing | nothing = nothing ≈-cong {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = let open ≡≡-Reasoning A in ≡≡-refl ≈-cong {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = let open ≡≡-Reasoning A in ≡≡-refl ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = let open ≡≡-Reasoning A in ≡≡-refl ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = let open ≡≡-Reasoning A in ≡≡-refl ≈-cong {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = let open ≡≡-Reasoning A in ≡≡-refl open ≈-Reasoning (MA) identity : {x : Obj I} → MA [ fmap ( id1 I x ) ≈ id1 MA (fobj x) ] identity {t0} = refl-hom identity {t1} = refl-hom distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → MA [ fmap (I [ g₁ o f₁ ]) ≈ MA [ fmap g₁ o fmap f₁ ] ] distr1 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1 distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = nothing distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = nothing distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = nothing distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = nothing distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = nothing distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = nothing distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = nothing distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = nothing distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = nothing distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = nothing distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = nothing distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = nothing distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = nothing distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = nothing distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = nothing distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = nothing distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = nothing distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = nothing distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = nothing distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = nothing distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = nothing distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = nothing distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = nothing distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym idL distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = nothing distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = nothing distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = nothing record Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field nil : {a b : Obj A } -> Hom A a b nil-idL : {a b c : Obj A } -> { f : Hom A a b } -> A [ A [ nil {b} {c} o f ] ≈ nil {a} {c} ] nil-idR : {a b c : Obj A } -> { f : Hom A b c } -> A [ A [ f o nil {a} {b} ] ≈ nil {a} {c} ] open Nil justFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> Nil A -> Functor (MaybeCat A ) A justFunctor{c₁} {c₂} {ℓ} A none = record { FObj = λ a → fobj a ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { identity = \{x} -> identity {x} ; distr = \ {a} {b} {c} {f} {g} -> distr2 {a} {b} {c} {f} {g} ; ≈-cong = \ {a} {b} {c} {f} -> ≈-cong {a} {b} {c} {f} } } where MA = MaybeCat A fobj : Obj MA -> Obj A fobj = \x -> x fmap : {x y : Obj MA } -> Hom MA x y -> Hom A x y fmap {x} {y} f with MaybeHom.hom f fmap {x} {y} _ | nothing = nil none fmap {x} {y} _ | (just f) = f identity : {x : Obj MA} -> A [ fmap (id1 MA x) ≈ id1 A (fobj x) ] identity = let open ≈-Reasoning (A) in refl-hom distr2 : {a : Obj MA} {b : Obj MA} {c : Obj MA} {f : Hom MA a b} {g : Hom MA b c} → A [ fmap (MA [ g o f ]) ≈ A [ fmap g o fmap f ] ] distr2 {a} {b} {c} {f} {g} with MaybeHom.hom f | MaybeHom.hom g distr2 | nothing | nothing = let open ≈-Reasoning (A) in sym ( nil-idR none ) distr2 | nothing | just ga = let open ≈-Reasoning (A) in sym ( nil-idR none ) distr2 | just fa | nothing = let open ≈-Reasoning (A) in sym ( nil-idL none ) distr2 | just f | just g = let open ≈-Reasoning (A) in refl-hom ≈-cong : {a : Obj MA} {b : Obj MA} {f g : Hom MA a b} → MA [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong {a} {b} {f} {g} eq with MaybeHom.hom f | MaybeHom.hom g ≈-cong {a} {b} {f} {g} nothing | nothing | nothing = let open ≈-Reasoning (A) in refl-hom ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq --- Equalizer --- f --- e ------> --- c ------> a b --- ^ / ------> --- |k h g --- | / --- | / ^ --- | / | --- |/ | Γ --- d _ | --- |\ | --- \ K af --- \ ------> --- \ t0 t1 --- ------> --- ag --- --- open Limit I' : {c₁ c₂ ℓ : Level} -> Category c₁ c₂ c₂ I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ} MA' : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) MA' {c₁} {c₂} {ℓ} {A} = MaybeCat A lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (lim : ( Γ : Functor (I' {c₁} {c₂} {ℓ}) (MA' {c₁} {c₂} {ℓ} {A}) ) → {a0 : Obj A } {u : NTrans I' MA' ( K MA' I' a0 ) Γ } → Limit MA' I' Γ a0 u ) -- completeness → {a b c : Obj A} (f g : Hom A a b ) → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g lim-to-equ {c₁} {c₂} {ℓ } A lim {a} {b} {c} f g e fe=ge = record { fe=ge = fe=ge ; k = λ {d} h fh=gh → k {d} h fh=gh ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' } where MA = MA' {c₁} {c₂} {ℓ} {A} I = I' {c₁} {c₂} {ℓ} mf : Hom MA a b mf = record { hom = just f } mg : Hom MA a b mg = record { hom = just g } Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g nmap : (x : Obj I ) ( d : Obj (MA) ) (h : Hom MA d a ) -> Hom MA (FObj (K MA I d) x) (FObj Γ x) nmap x d h with x | MaybeHom.hom h ... | _ | nothing = record { hom = nothing } ... | t0 | just jh = record { hom = just jh } ... | t1 | just jh = record { hom = just ( A [ f o jh ] ) } commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj MA) (h : Hom MA d a ) -> MA [ MA [ mf o h ] ≈ MA [ mg o h ] ] → MA [ MA [ FMap Γ f' o nmap x d h ] ≈ MA [ nmap y d h o FMap (K MA I d) f' ] ] commute1 {x} {y} {f'} d h fh=gh = {!!} nat : (d : Obj MA) → (h : Hom MA d a ) → MA [ MA [ mf o h ] ≈ MA [ mg o h ] ] → NTrans I MA (K MA I d) Γ nat d h fh=gh = record { TMap = λ x → nmap x d h ; isNTrans = record { commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh } } k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c k {d} h fh=gh with MaybeHom.hom ( limit (lim Γ {c} {nat c (record { hom = just e}) (just fe=ge) }) d (nat d (record { hom = just h }) (just fh=gh) ) ) k {d} h fh=gh | nothing = {!!} k {d} h fh=gh | just f = f ek=h : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> A [ A [ e o k h fh=gh ] ≈ h ] ek=h d h fh=gh = {!!} uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> ( k' : Hom A d c ) -> A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] uniquness d h fh=gh = {!!}