# HG changeset patch # User Shinji KONO # Date 1458730347 -32400 # Node ID dd086f5fb29f2b61f3aac5fb5777820e880c79db # Parent 28249d32b700d5ca7ab22390e6e5e863ded8d97b same conflict again ... diff -r 28249d32b700 -r dd086f5fb29f limit-to.agda --- a/limit-to.agda Wed Mar 23 17:16:29 2016 +0900 +++ b/limit-to.agda Wed Mar 23 19:52:27 2016 +0900 @@ -1,4 +1,4 @@ -open import Category -- https://github.com/konn/category-agda +open import Category -- https://github.com/konn/category-agda open import Level module limit-to where @@ -12,7 +12,7 @@ --- If we have limit then we have equalizer +-- If we have limit then we have equalizer --- two objects category --- --- f @@ -24,42 +24,73 @@ data TwoObject {c₁ : Level} : Set c₁ where - t0 : TwoObject - t1 : TwoObject + t0 : TwoObject + t1 : TwoObject + +data Arrow {ℓ : Level } : Set ℓ where + id-t0 : Arrow + id-t1 : Arrow + arrow-f : Arrow + arrow-g : Arrow record TwoHom {c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where field - hom : TwoObject {c₂ } + RawHom : Maybe ( Arrow {c₂} ) + +open TwoHom + +hom : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ (f : TwoHom {c₁} {c₂ } a b ) → Maybe ( Arrow {c₂} ) +hom {_} {_} {a} {b} f with RawHom f +hom {_} {_} {t0} {t0} _ | nothing = nothing +hom {_} {_} {t0} {t0} _ | just id-t0 = just id-t0 +hom {_} {_} {t1} {t1} _ | just id-t1 = just id-t1 +hom {_} {_} {t0} {t1} _ | just arrow-f = just arrow-f +hom {_} {_} {t0} {t1} _ | just arrow-g = just arrow-g +hom {_} {_} {_ } {_ } _ | _ = nothing + open TwoHom -- arrow composition -_×_ : ∀ {c₁ c₂} -> {a b c : TwoObject {c₁}} → Maybe ( TwoHom {c₁} {c₂} b c ) → Maybe ( TwoHom {c₁} {c₂} a b ) → Maybe ( TwoHom {c₁} {c₂} a c ) -_×_ nothing _ = nothing -_×_ (just _) nothing = nothing -_×_ {c₁} {c₂} {t1} {t1} {t1} _ f = f -_×_ {c₁} {c₂} {t0} {t0} {t0} f _ = f -_×_ {c₁} {c₂} {t0} {t1} {t1} _ f = f -_×_ {c₁} {c₂} {t0} {t0} {t1} f _ = f --- _×_ {c₁} {c₂} {t1} {t0} {t0} _ f = f --- _×_ {c₁} {c₂} {t1} {t1} {t0} f _ = f -_×_ {c₁} {c₂} {a} {b} {c} (just f) (just g) = 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 with hom f | hom g +... | nothing | _ = record { RawHom = nothing } +... | (just _) | nothing = record { RawHom = nothing } +... | (just id-t1) | (just arrow-f) = record { RawHom = just arrow-f } +... | (just id-t1) | (just arrow-g) = record { RawHom = just arrow-g } +... | (just id-t1) | (just id-t1 ) = record { RawHom = just id-t1 } +... | (just arrow-f) | (just id-t0) = record { RawHom = just arrow-f } +... | (just arrow-g) | (just id-t0) = record { RawHom = just arrow-g } +... | (just id-t0) | (just id-t0 ) = record { RawHom = just id-t0 } +... | (just _) | (just _) = record { RawHom = nothing } -_==_ : ∀{c₁ c₂ } { a b : TwoObject {c₁} } -> Rel (Maybe (TwoHom {c₁} {c₂ } a b )) (c₂) -_==_ = Eq _≡_ +_==_ : ∀{c₂ } -> Rel (Maybe (Arrow {c₂} )) (c₂) +_==_ = Eq _≡_ + +map2hom : ∀{ c₁ c₂ } -> {a b : TwoObject {c₁}} → Maybe ( Arrow {c₂} ) -> TwoHom {c₁} {c₂ } a b +map2hom {_} {_} {t1} {t1} (just id-t1) = record { RawHom = just id-t1 } +map2hom {_} {_} {t0} {t1} (just arrow-f) = record { RawHom = just arrow-f } +map2hom {_} {_} {t0} {t1} (just arrow-g) = record { RawHom = just arrow-g } +map2hom {_} {_} {t0} {t0} (just id-t0) = record { RawHom = just id-t0 } +map2hom {_} {_} {_} {_} _ = record { RawHom = nothing } -==refl : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x : Maybe (TwoHom {c₁} {c₂ } a b )} → x == x -==refl {_} {_} {_} {_} {just x} = just refl -==refl {_} {_} {_} {_} {nothing} = 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 ) -==sym : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x y : Maybe (TwoHom {c₁} {c₂ } a b )} → _==_ x y → _==_ y x +==refl : ∀{ c₂ } -> ∀ {x : Maybe (Arrow {c₂} )} → x == x +==refl {_} {just x} = just refl +==refl {_} {nothing} = nothing + +==sym : ∀{ c₂ } -> ∀ {x y : Maybe (Arrow {c₂} )} → _==_ x y → _==_ y x ==sym (just x≈y) = just (≡-sym x≈y) ==sym nothing = nothing -==trans : ∀{ c₁ c₂ } { a b : TwoObject {c₁} } -> ∀ {x y z : Maybe (TwoHom {c₁} {c₂ } a b ) } → +==trans : ∀{ c₂ } -> ∀ {x y z : Maybe (Arrow {c₂} ) } → x == y → y == z → x == z ==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z) ==trans nothing nothing = nothing @@ -72,23 +103,23 @@ infix 1 begin_ - data _IsRelatedTo_ { a b : TwoObject {c₁} } (x y : (Maybe (TwoHom {c₁} {c₂ } a b ))) : + data _IsRelatedTo_ (x y : (Maybe (Arrow {c₂} ))) : Set c₂ where relTo : (x≈y : x == y ) → x IsRelatedTo y - begin_ : { a b : TwoObject {c₁} } {x : Maybe (TwoHom {c₁} {c₂ } a b ) } {y : Maybe (TwoHom {c₁} {c₂ } a b )} → - x IsRelatedTo y → x == y + begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₂} ) } {y : Maybe (Arrow {c₂} )} → + x IsRelatedTo y → x == y begin relTo x≈y = x≈y - _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (TwoHom {c₁} {c₂ } a b )) {y z : Maybe (TwoHom {c₁} {c₂ } a b ) } → + _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₂} )) {y z : Maybe (Arrow {c₂} ) } → 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 (TwoHom {c₁} {c₂ } a b )) {y : Maybe (TwoHom {c₁} {c₂ } a b )} + _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₂} )) {y : Maybe (Arrow {c₂} )} → x IsRelatedTo y → x IsRelatedTo y _ ==⟨⟩ x≈y = x≈y - _∎ : { a b : TwoObject {c₁} }(x : Maybe (TwoHom {c₁} {c₂ } a b )) → x IsRelatedTo x + _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₂} )) → x IsRelatedTo x _∎ _ = relTo ==refl @@ -96,40 +127,73 @@ -- f g h -- d <- c <- b <- a -assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } - {f : Maybe (TwoHom {c₁} {c₂ } c d )} → - {g : Maybe (TwoHom {c₁} {c₂ } b c )} → - {h : Maybe (TwoHom {c₁} {c₂ } a b )} → - ( f × (g × h)) == ((f × g) × h ) -assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing -assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing -assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} with (just f × just g) -assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | nothing = ==refl -assoc-× {c₁} {c₂} {a} {b} {c} {d} {just f} {just g} {nothing} | just h = ==refl -assoc-× {_} {_} {t0} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t0} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t0} {t0} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t0} {t0} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t0} {t1} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t0} {t1} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t1} {t0} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t1} {t0} {t1} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t1} {t1} {t0} {just _} {just _} {just _} = ==refl -assoc-× {_} {_} {t1} {t1} {t1} {t1} {just _} {just _} {just _} = ==refl +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 +assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} | just _ | just _ | nothing = {!!} +assoc-× {c₁} {c₂} {t1} {t0} {_} {_} {f} {g} {h} | just _ | just _ | just _ = let open ==-Reasoning {c₁} {c₂} in + begin + {!!} + ==⟨ {!!} ⟩ + {!!} + ∎ +... | just _ | just _ | just _ = let open ==-Reasoning {c₁} {c₂} in + begin + {!!} + ==⟨ {!!} ⟩ + {!!} + ∎ +TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> (TwoHom {c₁} {c₂ } a a ) +TwoId {_} {_} t0 = record { RawHom = just id-t0 } +TwoId {_} {_} t1 = record { RawHom = just id-t1 } -TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> Maybe (TwoHom {c₁} {c₂ } a a ) -TwoId {_} {_} t0 = just record { hom = t0 } -TwoId {_} {_} t1 = just record { hom = t1 } - -open import maybeCat +open import maybeCat -- identityL {c₁} {c₂} {_} {b} {nothing} = let open ==-Reasoning {c₁} {c₂} in -- begin @@ -138,13 +202,13 @@ -- nothing -- ∎ -open import Relation.Binary +open import Relation.Binary TwoCat : {c₁ c₂ ℓ : Level } -> Category c₁ c₂ c₂ TwoCat {c₁} {c₂} {ℓ} = record { Obj = TwoObject {c₁} ; - Hom = λ a b → Maybe ( TwoHom {c₁} {c₂ } a b ) ; + Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; _o_ = \{a} {b} {c} x y -> _×_ {c₁ } { c₂} {a} {b} {c} x y ; - _≈_ = Eq _≡_ ; + _≈_ = \x y -> hom x == hom y ; Id = \{a} -> TwoId {c₁ } { c₂} a ; isCategory = record { isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ; @@ -152,35 +216,31 @@ 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 : Maybe ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) == f - identityL {c₁} {c₂} {t0} {t0} {nothing} = ==refl - identityL {c₁} {c₂} {t0} {t1} {nothing} = ==refl - identityL {c₁} {c₂} {t1} {t0} {nothing} = ==refl - identityL {c₁} {c₂} {t1} {t1} {nothing} = ==refl - identityL {_} {_} {t0} {t1} {just f} = ==refl - identityL {_} {_} {t1} {t1} {just f} = ==refl - identityL {_} {_} {t0} {t0} {just f} = {!!} - identityL {_} {_} {t1} {t0} {just f} = {!!} - identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : Maybe ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) == f - identityR {c₁} {c₂} {t0} {t0} {nothing} = ==refl - identityR {c₁} {c₂} {t0} {t1} {nothing} = ==refl - identityR {c₁} {c₂} {t1} {t0} {nothing} = ==refl - identityR {c₁} {c₂} {t1} {t1} {nothing} = ==refl - identityR {_} {_} {t0} {t0} {just f} = ==refl - identityR {_} {_} {t0} {t1} {just f} = ==refl - identityR {c₁} {c₂} {t1} {t0} {just f} = let open ==-Reasoning {c₁} {c₂} in + 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₂} {t0} {t0} {_} | just id-t0 = ==refl + identityL {c₁} {c₂} {t0} {t1} {_} | just id-t0 = let open ==-Reasoning {c₁} {c₂} in begin - (just f × TwoId t1) - ==⟨⟩ - nothing - ==⟨ {!!} ⟩ - just f - ∎ - identityR {_} {_} {t1} {t1} {just f} = {!!} - o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : Maybe ( TwoHom {c₁} {c₂ } A B)} {h i : Maybe ( TwoHom B C)} → - f == g → h == i → ( h × f ) == ( i × g ) + nothing + ==⟨ {!!} ⟩ + just ? + ∎ + identityL {c₁} {c₂} {_} {_} {_} | just id-t0 = {!!} + identityL {c₁} {c₂} {_} {_} {_} | just id-t1 = {!!} + identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl + identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl + identityL {c₁} {c₂} {_} {_} {_} | just arrow-f = {!!} + identityL {c₁} {c₂} {_} {_} {_} | just arrow-g = {!!} + identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) == hom f + identityR {c₁} {c₂} {_} {_} {_} = {!!} + 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-≈ {_} {_} {a} {b} {c} {f} {g} {h} {i} f≡g h≡i = {!!} @@ -190,8 +250,8 @@ ; 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} + ; 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₂} {ℓ} @@ -200,9 +260,9 @@ fobj : Obj I -> Obj A fobj t0 = a fobj t1 = b - fmap : {x y : Obj I } -> Maybe (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y) + fmap : {x y : Obj I } -> (TwoHom {c₁} {c₂} x y ) -> Hom MA (fobj x) (fobj y) fmap = {!!} - open ≈-Reasoning (A) + open ≈-Reasoning (A) identity : {x : Obj I} → {!!} identity {t0} = {!!} identity {t1} = {!!} @@ -218,17 +278,17 @@ --- c ------> a b --- ^ / ------> --- |k h g ---- | / ---- | / ---- | / ---- |/ ---- d +--- | / +--- | / +--- | / +--- |/ +--- d open Limit lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> (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} (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} f g e fe=ge = record { fe=ge = fe=ge @@ -240,14 +300,14 @@ Γ = {!!} 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 ] ] + 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 ] ] → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] commute1 {x} {y} {f'} d h fh=gh = {!!} nat : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ nat d h fh=gh = record { - TMap = λ x → nmap x d h ; + TMap = λ x → nmap x d h ; isNTrans = record { - commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} d h fh=gh + 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 @@ -257,6 +317,6 @@ 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 = {!!} + uniquness d h fh=gh = {!!}