Mercurial > hg > Members > kono > Proof > category

changeset 417:1e76e611d454

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
with inv-f, distribution law passed.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 24 Mar 2016 01:48:13 +0900
parents e4a2544d468c
children 7091104a8cb4
files limit-to.agda
diffstat 1 files changed, 279 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Wed Mar 23 22:47:32 2016 +0900
+++ b/limit-to.agda	Thu Mar 24 01:48:13 2016 +0900
@@ -7,7 +7,6 @@
 open import HomReasoning
 open import Relation.Binary.Core
 open import Data.Maybe
-open import maybeCat
 open Functor
 
 
@@ -28,31 +27,230 @@
    t0 : TwoObject
    t1 : TwoObject
 
+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 TwoCat  {ℓ c₁ c₂ : Level  } (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
-    field
-         obj→ : Obj A  -> TwoObject  { c₁}
-         hom→ : {a b : Obj A} -> Hom A a b -> TwoObject { c₁}
-         inv : {a b : Obj A} -> Hom A a b -> Hom A b a
-         iso→ : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ inv h o h ]  ≈  id1 A a ]
-         iso← : {a b : Obj A} -> ( h : Hom A a b ) -> A [ A [ h o inv h ]  ≈  id1 A b ]
-    obj← : TwoObject  {c₁} -> Obj A  
-    obj←  t0 = a
-    obj←  t1 = b
-    hom← :  TwoObject  {c₁} -> Hom A a b 
-    hom← t0 = f
-    hom← t1 = g
+record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set   c₂ where
+   field
+       RawHom   :   Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
+
+open TwoHom
+
+hom :  ∀{ c₁ c₂ }  {  a b : TwoObject  {c₁} } -> 
+       ∀ (f :  TwoHom {c₁}  {c₂ } a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
+hom {_} {_} {a} {b} f with RawHom  f
+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 {_} {_} {t1} {t0} _ | just inv-f = just inv-f
+hom {_} {_} {_ } {_ } _ | _ = nothing
+
+
+open TwoHom
+
+-- arrow composition
+
+
+_×_ :  ∀ {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
+_×_  {_}  {_}  {_} {_} {_} f g | nothing    | _                = record { RawHom =  nothing }
+_×_  {_}  {_}  {_} {_} {_} f g | just _     | nothing          = record { RawHom =  nothing }
+_×_  {_}  {_}  {t0} {t1} {t1} f g | just id-t1 | just arrow-f  = record { RawHom =  just arrow-f }
+_×_  {_}  {_}  {t0} {t1} {t1} f g | just id-t1 | just arrow-g  = record { RawHom =  just arrow-g }
+_×_  {_}  {_}  {t1} {t1} {t1} f g | just id-t1 | just id-t1    = record { RawHom =  just id-t1 }
+_×_  {_}  {_}  {t1} {t1} {t0} f g | just inv-f | just id-t1    = record { RawHom =  just inv-f }
+_×_  {_}  {_}  {t0} {t0} {t1} f g | just arrow-f | just id-t0    = record { RawHom =  just arrow-f }
+_×_  {_}  {_}  {t0} {t0} {t1} f g | just arrow-g | just id-t0    = record { RawHom =  just arrow-g }
+_×_  {_}  {_}  {t0} {t0} {t0} f g | just id-t0 | just id-t0    = record { RawHom =  just id-t0 }
+_×_  {_}  {_}  {t1} {t0} {t0} f g | just id-t0 | just inv-f    = record { RawHom =  just inv-f }
+_×_  {_}  {_}  {_} {_} {_} f g | just _ | just _   = record { RawHom =  nothing }
+
+
+_==_ :  ∀{ c₁ c₂ a b }   ->  Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂)
+_==_   =  Eq   _≡_
 
-open TwoCat
+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 { 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 }
+
+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 )
+
+==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
+
+
+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
+
 
 
-open MaybeHom
+--          f    g    h
+--       d <- c <- b <- a
+
+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
+                   {!!}
+                ==⟨ {!!}  ⟩
+                  {!!}
+                ∎
 
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) ->  
-    TwoCat A a b f g ->
-    Functor A (MaybeCat A )
-indexFunctor  {c₁} {c₂} {ℓ} A  a b f g two = record {
+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 }
+
+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-≈  {_} {_} {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = {!!}
+
+
+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 {
@@ -61,39 +259,66 @@
              ; ≈-cong = \ {a} {b} {c} {f}   -> ≈-cong  {a} {b} {c} {f}
        }
       } where
+          I = TwoCat  {c₁} {c₂} {ℓ}
           MA = MaybeCat A
           open ≈-Reasoning (MA)
-          fobj :  Obj A -> Obj A
-          fobj x with obj→ two x
-          fobj _ | t0 = a
-          fobj _ | t1 = b
-          fmap :  {x y : Obj A } ->  (Hom A  x y  ) -> Hom MA (fobj x) (fobj y)
-          fmap  {x} {y} h with  obj→ two x |  obj→ two y | hom→ two f
-          fmap  {_} {_} h | t0 | t1 | t0 = record { hom = just f }
-          fmap  {_} {_} h | t0 | t1 | t1 = record { hom = just g }
-          fmap  {_} {_} h | t1 | t0 | t0 = record { hom = just (inv two f) }
-          fmap  {_} {_} h | t1 | t0 | t1 = record { hom = just (inv two g) }
-          fmap  {x} {_} h | t0 | t0 | _ = id1 MA ( obj←  two t0 )
-          fmap  {x} {_} h | t1 | t1 | _ = id1 MA ( obj←  two t1 )
-          identity :  {x : Obj A} → MA [ fmap ( id1 A x  )  ≈  id1 MA ( fobj x )  ]
-          identity {x} with  obj→ two x
-          identity | t0  = refl-hom 
-          identity | t1  = refl-hom 
-          distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →  
-                MA [ fmap (A [ g₁ o f₁ ]) ≈  MA [ fmap g₁ o fmap f₁ ] ]
-          distr1 {a1} {b1} {c} {f1} {g1} with  obj→ two a1 |  obj→ two b1  | obj→ two c | hom→ two f | hom→ two g 
-          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t0 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t1 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t1 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t1 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t0 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t0 | _ | _ =  {!!}
-          -- next  two cases require the inverse of f and g
-          -- if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
-          --    so A [ g o  f ] should be nothing in codomain Category
-          distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t1 | _ | _ =  {!!}
-          distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t0 | _ | _ =  {!!}
-          ≈-cong :   {a : Obj A} {b : Obj A} {f g : Hom A a b}  → _[_≈_] A f g → {!!}
+          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 }
+          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
+
+          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → _[_≈_] I f g → {!!}
           ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}
 
 
@@ -119,9 +344,9 @@
         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 = A
-         MA = MaybeCat A
+        ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
+     } where
+         I = TwoCat {c₁} {c₂} {ℓ }
          Γ = {!!}
          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 = {!!}