# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1457962547 -32400
# Node ID a0ab2643eee7904d65a0c762f207aae3759af0eb
# Parent  2f59c2db9d98bcd401859b24b09c27e155864f35
on going ...

diff -r 2f59c2db9d98 -r a0ab2643eee7 limit-to.agda
--- a/limit-to.agda	Mon Mar 14 20:33:58 2016 +0900
+++ b/limit-to.agda	Mon Mar 14 22:35:47 2016 +0900
@@ -159,33 +159,55 @@
         associative {_} {_} {_} {_} {_} {_} {_} | just arrow-g | just arrow-g | just arrow-g =  refl
 
 indexFunctor :  {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
-        ( a b : Obj A ) ( f g : Hom A a b )  ->  Functor TwoCat A
-indexFunctor A a b f g = record {
+        ( a b : Obj A ) ( f g : Hom A a b )  ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) A
+indexFunctor  {c₁} {c₂} {ℓ} A a b f g nf nf-rev nidA nidB = record {
          FObj = λ a → fobj a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
              identity = \{x} -> identity {x}
-             ; distr = \ {a} {b} {c} {f} {g}   -> distr {a} {b} {c} {f} {g} 
+             ; distr = \ {a} {b} {c} {f} {g}   -> distr1 {a} {b} {c} {f} {g} 
              ; ≈-cong = {!!}
        }
       } where
-          I = TwoCat
-          fobj :  Obj TwoCat -> Obj A
+          I = TwoCat  {c₁} {c₂} {ℓ}
+          fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
+          fmap1 :  {x y : Obj I } -> Hom I x y -> Maybe Arrow -> Hom A (fobj x) (fobj y)
+          fmap1 {t0} {t1} x  ( just arrow-f ) = f
+          fmap1 {t0} {t1} x  ( just arrow-g ) = g
+          fmap1 {t0} {t1} x   _ = nf
+          fmap1 {t0} {t0} x   _ = id1 A a
+          fmap1 {t1} {t1} x   _ = id1 A b
+          fmap1 {t1} {t0} x   _ = nf-rev
           fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y)
-          fmap {X} {Y} x with Map x
-          fmap {t0} {t1} x  | just arrow-f = f
-          fmap {t0} {t1} x  | just arrow-g = g
-          fmap {t0} {t0} x  | just id-t0 = id1 A a
-          fmap {t1} {t1} x  | just id-t0 = id1 A b
-          fmap {_} {_} x  | _ = {!!}
+          fmap {x} {y} f  = fmap1 {x} {y} f ( Map f)
+          open ≈-Reasoning (A) 
           identity :  {x : Obj I} → A [ fmap (id1 I  x) ≈ id1 A  (fobj x) ]
-          identity    = {!!}
-          distr : {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₁ ] ]
-          distr {a₁} {b₁} {c} {f₁} {g₁}  = {!!}
+          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 {t0} {t0} {t0} {f1} {g1}  = sym idL
+          distr1 {t1} {t0} {t0} {f1} {g1}  = sym idL
+          distr1 {t1} {t1} {t0} {f1} {g1}  = sym idR
+          distr1 {t1} {t1} {t1} {f1} {g1}  = sym idR
+          distr1 {a1} {b1} {c} {f1} {g1}  with Map f1 | Map g1
+          distr1 {t0} {t1} {t1} {f1} {g1} | fa  | just arrow-f  = begin
+                    fmap1 {!!} ( twocomp (just arrow-f)  fa )
+                ≈⟨ {!!} ⟩
+                    fmap1 f1 fa
+                ≈⟨ sym idL  ⟩
+                    id1 A b  o fmap1 f1 fa
+                ≈⟨⟩
+                    fmap1 g1 (just arrow-f)  o fmap1 f1 fa
+                ∎ 
+          distr1 {a1} {b1} {c} {f1} {g1}  | _ | _ = {!!}
           ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
-          ≈-cong {a} {b} {f} {g}  f≈g = let open ≈-Reasoning (A) in {!!}
+          ≈-cong {t0} {t0} {f1} {g1}  f≈g = refl-hom
+          ≈-cong {t1} {t1} {f1} {g1}  f≈g = refl-hom
+          ≈-cong {t1} {t0} {f1} {g1}  f≈g = refl-hom
+          ≈-cong {t0} {t1} {f1} {g1}  f≈g = ≡-cong f≈g (\x -> fmap1 g1 x)     
+
 
 ---  Equalizer
 ---                     f
@@ -201,18 +223,18 @@
 
 open Limit
 
-lim-to-equ : {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
+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} ( 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 ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ A lim {a} {b} {c}  f g e fe=ge = record {
+lim-to-equ {c₁} {c₂} {ℓ } A lim {a} {b} {c} nf nf-rev nidA nidB  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
-         Γ = indexFunctor A a b f g 
+         I = TwoCat {c₁} {c₂} {ℓ }
+         Γ = indexFunctor A a b f g nf nf-rev nidA nidB
          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 ] ]