Members/kono/Proof/category: limit-to.agda comparison

comparison limit-to.agda @ 417:1e76e611d454

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

comparison

equal deleted inserted replaced

-:e4a2544d468c
+:1e76e611d454
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary.Core
 open import Data.Maybe
-open import maybeCat
 open Functor
 data  TwoObject {c₁ : Level}  : Set c₁ where
 t0 : TwoObject
 t1 : TwoObject
+data Arrow {c₁ c₂ : Level } ( t00 t11 :  TwoObject {c₁} ) : TwoObject {c₁}  -> TwoObject {c₁} -> Set c₂ where
-record TwoCat  {ℓ c₁ c₂ : Level  } (A : Category  c₁ c₂ ℓ)  ( a b : Obj A ) ( f g : Hom A a b ): Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
+id-t0 : Arrow t00 t11 t00 t00
-field
+id-t1 : Arrow t00 t11 t11 t11
-obj→ : Obj A  -> TwoObject  { c₁}
+arrow-f :  Arrow t00 t11 t00 t11
-hom→ : {a b : Obj A} -> Hom A a b -> TwoObject { c₁}
+arrow-g :  Arrow t00 t11 t00 t11
-inv : {a b : Obj A} -> Hom A a b -> Hom A b a
+inv-f :  Arrow t00 t11 t11 t00
-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 ]
+record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set   c₂ where
-obj← : TwoObject  {c₁} -> Obj A
+field
-obj←  t0 = a
+RawHom   :   Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
-obj←  t1 = b
-hom← :  TwoObject  {c₁} -> Hom A a b
+open TwoHom
-hom← t0 = f
-hom← t1 = g
+hom :  ∀{ c₁ c₂ }  {  a b : TwoObject  {c₁} } ->
+∀ (f :  TwoHom {c₁}  {c₂ } a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b )
-open TwoCat
+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
-open MaybeHom
+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
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) ->
+hom {_} {_} {_ } {_ } _ | _ = nothing
-TwoCat A a b f g ->
-Functor A (MaybeCat A )
-indexFunctor  {c₁} {c₂} {ℓ} A  a b f g two = record {
+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   _≡_
+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
+--          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
+{!!}
+==⟨ {!!}  ⟩
+{!!}
+∎
+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 {
 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
 open ≈-Reasoning (MA)
-fobj :  Obj A -> Obj A
+fobj :  Obj I -> Obj A
-fobj x with obj→ two x
+fobj t0 = a
-fobj _ | t0 = a
+fobj t1 = b
-fobj _ | t1 = b
+fmap :  {x y : Obj I } ->  (TwoHom {c₁}  {c₂} x y  ) -> Hom MA (fobj x) (fobj y)
-fmap :  {x y : Obj A } ->  (Hom A  x y  ) -> Hom MA (fobj x) (fobj y)
+fmap  {x} {y} h with hom h
-fmap  {x} {y} h with  obj→ two x |  obj→ two y | hom→ two f
+fmap  {t0} {t0} h | just id-t0 = id1 MA a
-fmap  {_} {_} h | t0 | t1 | t0 = record { hom = just f }
+fmap  {t1} {t1} h | just id-t1 = id1 MA b
-fmap  {_} {_} h | t0 | t1 | t1 = record { hom = just g }
+fmap  {t0} {t1} h | just arrow-f = record { hom = just f }
-fmap  {_} {_} h | t1 | t0 | t0 = record { hom = just (inv two f) }
+fmap  {t0} {t1} h | just arrow-g = record { hom = just g }
-fmap  {_} {_} h | t1 | t0 | t1 = record { hom = just (inv two g) }
+fmap  {_} {_} h | _  = record { hom = nothing }
-fmap  {x} {_} h | t0 | t0 | _ = id1 MA ( obj←  two t0 )
+identity :  {x : Obj I} → MA [ fmap ( id1 I x ) ≈  id1 MA (fobj x) ]
-fmap  {x} {_} h | t1 | t1 | _ = id1 MA ( obj←  two t1 )
+identity {t0}  =  refl-hom
-identity :  {x : Obj A} → MA [ fmap ( id1 A x  )  ≈  id1 MA ( fobj x )  ]
+identity {t1}  =  refl-hom
-identity {x} with  obj→ two x
+distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} →
-identity | t0  = refl-hom
+MA [ fmap (I [ g₁ o f₁ ])  ≈  MA [ fmap g₁ o fmap f₁ ] ]
-identity | t1  = refl-hom
+distr1 {a1} {b1} {c1} {f1} {g1}   with hom g1 | hom f1
-distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} →
+distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing   =  nothing
-MA [ fmap (A [ g₁ o f₁ ]) ≈  MA [ fmap g₁ o fmap f₁ ] ]
+distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} with  obj→ two a1 |  obj→ two b1  | obj→ two c | hom→ two f | hom→ two g
+distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t0 | _ | _ =  {!!}
+distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t0 | t1 | _ | _ =  {!!}
+distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t1 | _ | _ =  {!!}
+distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t1 | _ | _ =  {!!}
+distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t0 | _ | _ =  {!!}
+distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t1 | t0 | _ | _ =  {!!}
+distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0   =  nothing
--- next  two cases require the inverse of f and g
+distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0   =  nothing
--- if we add invserse, there no nothing part, it generates extra commutaivitiy in nat, which is no good
+distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1   =  nothing
---    so A [ g o  f ] should be nothing in codomain Category
+distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t1 | t0 | t1 | _ | _ =  {!!}
+distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f   =  nothing
-distr1 {a1} {b1} {c} {f1} {g1} |  t0 | t1 | t0 | _ | _ =  {!!}
+distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f   =  nothing
-≈-cong :   {a : Obj A} {b : Obj A} {f g : Hom A a b}  → _[_≈_] A f g → {!!}
+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 = {!!}
 ---  Equalizer
 ---                     f
 → (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
+; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
-I = A
+} where
-MA = MaybeCat A
+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 = {!!}
 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' ] ]

Mercurial > hg > Members > kono > Proof > category

comparison limit-to.agda @ 417:1e76e611d454