Mercurial > hg > Members > kono > Proof > category

changeset 415:dd086f5fb29f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
same conflict again ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 23 Mar 2016 19:52:27 +0900
parents 28249d32b700
children e4a2544d468c
files limit-to.agda
diffstat 1 files changed, 163 insertions(+), 103 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}