Mercurial > hg > Members > kono > Proof > category
changeset 401:e4c10d6375f6
Maybe Category to-limit
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 17 Mar 2016 10:58:01 +0900 |
| parents | 89785764bccb |
| children | 9123f79c0642 |
| files | limit-to.agda |
| diffstat | 1 files changed, 52 insertions(+), 236 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Thu Mar 17 08:34:10 2016 +0900 +++ b/limit-to.agda Thu Mar 17 10:58:01 2016 +0900 @@ -1,15 +1,17 @@ open import Category -- https://github.com/konn/category-agda open import Level -module limit-to where +module limit-to { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where open import cat-utility open import HomReasoning open import Relation.Binary.Core -open import Data.Maybe.Core +open import Data.Maybe open Functor + + -- If we have limit then we have equalizer --- two objects category --- @@ -43,85 +45,35 @@ open Two-Hom -Map : {c₁ ℓ : Level } -> (a b : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a b -> Maybe ( Arrow {ℓ } ) -Map f with hom f -Map f | nothing = nothing -Map _ | just f = RawMap f - Two-id : {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) -> Two-Hom {c₁} { ℓ} a a -Two-id _ = record { hom = record { RawMap = id-t0 } ; arrow-iso = refl } +Two-id _ = record { hom = just ( record { RawMap = id-t0 } ) } -- arrow composition -twocomp : {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Maybe (Arrow {ℓ } ) -twocomp id-t0 f = just f -twocomp f id-t0 = just f +twocomp : {c₁ ℓ : Level } -> { a b : TwoObject {c₁} } -> Arrow {ℓ } -> Arrow {ℓ } -> Maybe ( RawHom a b ) +twocomp id-t0 f = just ( record { RawMap = f } ) +twocomp f id-t0 = just ( record { RawMap = f } ) twocomp _ _ = nothing -twocmp-associative : {ℓ : Level } -> ( f : Arrow {ℓ } ) -> ( g : Arrow {ℓ } ) -> ( h : Arrow {ℓ } ) → twocomp f (twocomp g h) ≡ twocomp (twocomp f g) h -twocmp-associative id-t0 _ _ = refl -twocmp-associative arrow-f id-t0 _ = refl -twocmp-associative arrow-f arrow-f id-t0 = refl -twocmp-associative arrow-f arrow-f arrow-f = refl -twocmp-associative arrow-f arrow-f arrow-g = refl -twocmp-associative arrow-f arrow-f nil = refl -twocmp-associative arrow-g id-t0 _ = refl -twocmp-associative arrow-f arrow-g nil = refl -twocmp-associative arrow-f arrow-g id-t0 = refl -twocmp-associative arrow-f arrow-g arrow-f = refl -twocmp-associative arrow-f arrow-g arrow-g = refl -twocmp-associative arrow-f nil nil = refl -twocmp-associative arrow-f nil id-t0 = refl -twocmp-associative arrow-f nil arrow-f = refl -twocmp-associative arrow-f nil arrow-g = refl -twocmp-associative arrow-g arrow-f nil = refl -twocmp-associative arrow-g arrow-f id-t0 = refl -twocmp-associative arrow-g arrow-f arrow-f = refl -twocmp-associative arrow-g arrow-f arrow-g = refl -twocmp-associative arrow-g arrow-g nil = refl -twocmp-associative arrow-g arrow-g id-t0 = refl -twocmp-associative arrow-g arrow-g arrow-f = refl -twocmp-associative arrow-g arrow-g arrow-g = refl -twocmp-associative arrow-g nil nil = refl -twocmp-associative arrow-g nil id-t0 = refl -twocmp-associative arrow-g nil arrow-f = refl -twocmp-associative arrow-g nil arrow-g = refl -twocmp-associative nil id-t0 _ = refl -twocmp-associative nil nil nil = refl -twocmp-associative nil nil id-t0 = refl -twocmp-associative nil nil arrow-f = refl -twocmp-associative nil nil arrow-g = refl -twocmp-associative nil arrow-f nil = refl -twocmp-associative nil arrow-f id-t0 = refl -twocmp-associative nil arrow-f arrow-f = refl -twocmp-associative nil arrow-f arrow-g = refl -twocmp-associative nil arrow-g nil = refl -twocmp-associative nil arrow-g id-t0 = refl -twocmp-associative nil arrow-g arrow-f = refl -twocmp-associative nil arrow-g arrow-g = refl +_×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C +_×_ { c₁} {ℓ} {a} {b} {c} f g with hom f | hom g +_×_ { c₁} {ℓ} {a} {b} {c} f g | nothing | _ = record { hom = nothing } +_×_ { c₁} {ℓ} {a} {b} {c} f g | _ | nothing = record { hom = nothing } +_×_ { c₁} {ℓ} {a} {b} {c} _ _ | just f | just g = record { hom = twocomp { c₁} {ℓ} {a} {c} (RawMap f) (RawMap g ) } + +_==_ : {c₁ ℓ : Level } -> {a b : TwoObject {c₁} } -> Rel (Maybe (RawHom {c₁} {ℓ} a b )) (ℓ ⊔ c₁) +_==_ = Eq ( _≡_ ) -_×_ : { c₁ ℓ : Level } -> {A B C : TwoObject { c₁} } → Two-Hom { c₁} {ℓ} B C → Two-Hom { c₁} {ℓ} A B → Two-Hom { c₁} {ℓ} A C -_×_ { c₁} {ℓ} {a} {b} {c} f g with hom f | hom g -_×_ { c₁} {ℓ} {a} {b} {c} f g | nothing | _ = record { hom = nothing } -_×_ { c₁} {ℓ} {a} {b} {c} f g | _ | nothig = record { hom = nothing } -_×_ { c₁} {ℓ} {a} {b} {c} _ _ | just f | just g = comp f g - where - comp : {a c : TwoObject {c₁}} (f : Arrow {ℓ}) -> (g : Arrow {ℓ}) -> Two-Hom { c₁} {ℓ} a c - comp f g with ( twocomp {ℓ} ( RawMap f) ( RawMap g) ) - comp f g | nothing = record { hom = nothing } - comp f g | just h = record { hom = record { RawMap = h } } - - -TwoCat : { c₁ c₂ ℓ : Level } -> Category c₁ (ℓ ⊔ c₁) ℓ +TwoCat : { c₁ c₂ ℓ : Level } -> Category c₁ (ℓ ⊔ c₁) (ℓ ⊔ c₁) TwoCat {c₁} {c₂} {ℓ} = record { Obj = TwoObject {c₁} ; Hom = λ a b → Two-Hom {c₁ } { ℓ} a b ; _o_ = _×_ { c₁} {ℓ} ; - _≈_ = λ a b → Map a ≡ Map b ; + _≈_ = λ a b → hom a == hom b ; Id = \{a} -> Two-id a ; isCategory = record { - isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}; + isEquivalence = record {refl = ? ; trans = ? ; 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} ; @@ -130,49 +82,20 @@ } where open import Relation.Binary.PropositionalEquality ≡-cong = Relation.Binary.PropositionalEquality.cong - identityL : {A B : TwoObject} {f : Two-Hom A B} → Map ( Two-id B × f ) ≡ Map f - identityL {a} {b} {f} with Map f - identityL {_} {_} {f} | id-t0 = refl - identityL {_} {_} {f} | arrow-f = refl - identityL {_} {_} {f} | arrow-g = refl - identityL {_} {_} {f} | nil = refl - identityR : {A B : TwoObject} {f : Two-Hom A B} → Map ( f × Two-id A ) ≡ Map f - identityR {a} {b} {f} with Map f - identityR {_} {_} {f} | id-t0 = refl - identityR {_} {_} {f} | arrow-f = refl - identityR {_} {_} {f} | arrow-g = refl - identityR {_} {_} {f} | nil = refl + identityL : {A B : TwoObject} {f : Two-Hom A B} → hom ( Two-id B × f ) == hom f + identityL {a} {b} {f} = ? + identityR : {A B : TwoObject} {f : Two-Hom A B} → hom ( f × Two-id A ) == hom f + identityR {a} {b} {f} = ? o-resp-≈ : {A B C : TwoObject} {f g : Two-Hom A B} {h i : Two-Hom B C} → - Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g ) - o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = let open ≡-Reasoning in - begin - Map (h × f) - ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom {_} {_} {a} {c} ( twocomp (Map h) x ) ) ) f≡g ⟩ - Map (h × g) - ≡⟨ ≡-cong (\x -> RawMap ( arrow2hom {_} {_} {a} {c} ( twocomp x (Map g) ) ) ) h≡i ⟩ - Map (i × g) - ∎ - associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h ) - associative {_} {_} {_} {_} {f} {g} {h} = let open ≡-Reasoning in - begin - Map ( f × (g × h) ) - ≡⟨⟩ - twocomp (RawMap (hom f)) (twocomp (RawMap (hom g)) (RawMap (hom h))) - ≡⟨ twocmp-associative (RawMap (hom f)) (RawMap (hom g)) (RawMap (hom h)) ⟩ - twocomp (twocomp (RawMap (hom f)) (RawMap (hom g))) (RawMap (hom h)) - ≡⟨⟩ - Map ( (f × g) × h ) - ∎ + hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g ) + o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = ? + associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → hom ( f × (g × h) ) == hom ( (f × g) × h ) + associative {_} {_} {_} {_} {f} {g} {h} = ? +open import maybeCat {c₁} {c₂} {ℓ} {A } -indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( a b : Obj A ) ( f g h : Hom A a b ) ( h' : Hom A b a ) - ( f-iso : A [ A [ f o f' ] ≈ id1 A b ]) - ( f'-iso : A [ A [ f' o f ] ≈ id1 A a ]) - ( g-iso : A [ A [ g o f' ] ≈ id1 A b ]) - ( g'-iso : A [ A [ f' o g ] ≈ id1 A a ]) - -> Functor (TwoCat {c₁} {c₂} {ℓ} ) A -indexFunctor {c₁} {c₂} {ℓ} A a b f g h h' f-iso f'-iso g-iso g'-iso = record { +indexFunctor : {c₁ c₂ ℓ : Level} ( a b : Obj MaybeCat ) ( f g : Hom A a b ) -> Functor (TwoCat {c₁} {c₂} {ℓ} ) (MaybeCat ) +indexFunctor {c₁} {c₂} {ℓ} a b f g = record { FObj = λ a → fobj a ; FMap = λ f → fmap f ; isFunctor = record { @@ -185,132 +108,25 @@ fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b - fmap1 : {x y : Obj I } -> Arrow -> Hom A (fobj x) (fobj y) - fmap1 {t0} {t1} arrow-f = f - fmap1 {t0} {t1} arrow-g = g - fmap1 {t0} {t0} id-t0 = id1 A a - fmap1 {t1} {t1} id-t0 = id1 A b - fmap1 {t0} {t0} _ = id1 A a - fmap1 {t1} {t1} _ = id1 A b - fmap1 {t0} {t1} nil = h - fmap1 {t0} {t1} id-t0 = h - fmap1 {t1} {t0} nil = h' - fmap1 {t1} {t0} id-t0 = h' - fmap1 {t1} {t0} arrow-f = h' - fmap1 {t1} {t0} arrow-g = h' - fmap : {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y) - fmap {x} {y} f = fmap1 {x} {y} ( Map f) + fmap1 : {x y : Obj I } -> (Arrow {ℓ} ) -> Hom MaybeCat (fobj x) (fobj y) + fmap1 {t0} {t1} arrow-f = record { hom = just f } + fmap1 {t0} {t1} arrow-g = record { hom = just g } + fmap1 {t0} {t0} id-t0 = record { hom = just ( id1 A a )} + fmap1 {t1} {t1} id-t0 = record { hom = just ( id1 A b )} + fmap1 {_} {_} _ = record { hom = nothing } + fmap : {x y : Obj I } -> Hom I x y -> Hom MaybeCat (fobj x) (fobj y) + fmap {x} {y} f with ( hom f ) + fmap {x} {y} f | nothing = record { hom = nothing } + fmap {x} {y} _ | just f = fmap1 {x} {y} ( RawMap f ) open ≈-Reasoning (A) - identity : {x : Obj I} → A [ fmap (id1 I x) ≈ id1 A (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} → A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] - distr1 {a1} {b1} {c} {f1} {g1} with Map f1 | Map g1 - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-f = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | arrow-g = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | id-t0 = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-f | nil = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | id-t0 = sym g'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-f = sym g'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | arrow-g = sym g'-iso - distr1 {t0} {t1} {t0} {_} {_} | arrow-g | nil = sym g'-iso - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-f = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | arrow-g = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | id-t0 = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | id-t0 | nil = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | nil | arrow-f = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | nil | arrow-g = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | nil | id-t0 = sym f'-iso - distr1 {t0} {t1} {t0} {_} {_} | nil | nil = sym f'-iso - - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | id-t0 = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-f = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | arrow-g = sym g-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-f | nil = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | id-t0 = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-f = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | arrow-g = sym g-iso - distr1 {t1} {t0} {t1} {_} {_} | arrow-g | nil = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | nil = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-f = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | arrow-g = sym g-iso - distr1 {t1} {t0} {t1} {_} {_} | id-t0 | id-t0 = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | nil | nil = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | nil | arrow-f = sym f-iso - distr1 {t1} {t0} {t1} {_} {_} | nil | arrow-g = sym g-iso - distr1 {t1} {t0} {t1} {_} {_} | nil | id-t0 = sym f-iso - - distr1 {_} {t0} {t0} {f1} {g1} | fa | id-t0 = sym idL -- * - distr1 {t1} {t1} {t0} {f1} {g1} | id-t0 | ga = sym idR -- * - - distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | id-t0 = sym idR -- * - distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | nil = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | arrow-f = sym idR -- * - distr1 {t1} {t1} {t1} {f1} {g1} | id-t0 | arrow-g = sym idR -- * - - distr1 {t1} {t1} {t0} {f1} {g1} | nil | ga = sym idR - distr1 {t1} {t1} {t0} {f1} {g1} | arrow-f | ga = sym idR - distr1 {t1} {t1} {t0} {f1} {g1} | arrow-g | ga = sym idR - distr1 {t1} {t0} {t0} {f1} {g1} | fa | nil = sym idL - distr1 {t1} {t0} {t0} {f1} {g1} | fa | arrow-f = sym idL - distr1 {t1} {t0} {t0} {f1} {g1} | fa | arrow-g = sym idL - - distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | arrow-f = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | arrow-g = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | id-t0 | nil = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | nil | arrow-f = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | nil | arrow-g = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | nil | nil = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | nil = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | arrow-f = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-f | arrow-g = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | nil = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | arrow-f = sym idR - distr1 {t0} {t0} {t0} {f1} {g1} | arrow-g | arrow-g = sym idR - - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | id-t0 = sym idR -- * - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | nil = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | arrow-f = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-f | arrow-g = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | id-t0 = sym idR -- * - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | nil = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | arrow-f = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | arrow-g | arrow-g = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | nil | id-t0 = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | nil | nil = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | nil | arrow-g = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | nil | arrow-f = sym idR - - distr1 {t0} {t0} {t1} {f1} {g1} | nil | arrow-f = sym idR - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | arrow-f = sym idR - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | arrow-f = sym idR - distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | arrow-f = sym idR -- * - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-f | arrow-g = {!!} - distr1 {t0} {t0} {t1} {f1} {g1} | arrow-g | arrow-g = {!!} - distr1 {t0} {t0} {t1} {f1} {g1} | id-t0 | arrow-g = sym idR -- * - distr1 {t0} {t0} {t1} {f1} {g1} | nil | arrow-g = begin - f - ≈⟨ {!!} ⟩ - g o id1 A a - ≈⟨⟩ - g o fmap1 {t0} {t0} nil - ≈⟨⟩ - fmap1 {t0} {t1} arrow-g o fmap1 {t0} {t0} nil - ∎ - distr1 {t0} {t0} {t1} {f1} {g1} | fa | ga-g = {!!} - distr1 {t0} {t1} {t1} {f1} {g1} | nil | arrow-f = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | nil | arrow-g = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | arrow-f | id-t0 = sym idL -- * - distr1 {t0} {t1} {t1} {f1} {g1} | arrow-g | id-t0 = sym idL -- * - distr1 {t0} {t1} {t1} {f1} {g1} | arrow-g | arrow-g = {!!} - distr1 {t0} {t1} {t1} {f1} {g1} | fa | ga = begin - {!!} - ≈⟨ {!!} ⟩ - fmap1 {t1} {t1} ga o fmap1 {t0} {t1} fa - ∎ - - ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {_} {_} {f1} {g1} f≈g = ≡-cong f≈g (\x -> fmap1 x) + identity : {x : Obj I} → MaybeCat [ fmap (id1 I x) ≈ id1 MaybeCat (fobj x) ] + identity {t0} = ? + identity {t1} = ? + distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → + MaybeCat [ fmap (I [ g₁ o f₁ ]) ≈ MaybeCat [ fmap g₁ o fmap f₁ ] ] + distr1 {a1} {b1} {c} {f1} {g1} = ? + ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → MaybeCat [ fmap f ≈ fmap g ] + ≈-cong {_} {_} {f1} {g1} f≈g = ? --- Equalizer @@ -327,18 +143,18 @@ open Limit -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) +lim-to-equ : (lim : (I : Category c₁ c₂ ℓ) ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness - → {a b c : Obj A} ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) (f g : Hom A a b ) + → {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} nf nf-rev nidA nidB f g e fe=ge = record { +lim-to-equ 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 I = TwoCat {c₁} {c₂} {ℓ } - Γ = indexFunctor A a b f g {!!} {!!} {!!} {!!} {!!} + Γ = ? nmap : (x : Obj I) ( d : Obj A ) (h : Hom A d a ) -> Hom A (FObj (K A I d) x) (FObj Γ x) nmap x d h = {!!} commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) -> A [ A [ f o h ] ≈ A [ g o h ] ]