# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1458972559 -32400
# Node ID 02eefa110eaef91a6fbb61c645929b8ad4287fc4
# Parent  7f8b9f1f1bba32c6d9053301606fea709640c3f9
nat commute in limit-to

diff -r 7f8b9f1f1bba -r 02eefa110eae limit-to.agda
--- a/limit-to.agda	Sat Mar 26 13:50:18 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 15:09:19 2016 +0900
@@ -292,6 +292,7 @@
 record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where
      field 
          nil : {a b : Obj A } -> Hom A a b
+         nil-id : {a  : Obj A } ->  A [ nil {a} {a} ≈ id1 A a ]
          nil-idL : {a b c : Obj A } -> { f : Hom A a b } -> A [ A [ nil {b} {c} o f ]   ≈ nil {a} {c} ]
          nil-idR : {a b c : Obj A } -> { f : Hom A b c } -> A [ A [ f o nil {a} {b} ]   ≈ nil {a} {c} ]
 
@@ -328,7 +329,7 @@
           ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq
 
 
-indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) A
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) A
 indexFunctor  {c₁} {c₂} {ℓ} A none a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
@@ -446,61 +447,103 @@
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
          open  ≈-Reasoning A
+         I : Category c₁ c₂  c₂ 
          I = I'   {c₁} {c₂} {ℓ} 
+         Γ : Functor I A
          Γ = indexFunctor  {c₁} {c₂} {ℓ} A  none a b f g
          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 with x 
          ... | t0 = h
          ... | t1 =  A [ f o  h ] 
-         commute1 : {x y : Obj I}  {f' : Hom I x y} { ar : Maybe ( Arrow  {c₁} {c₂} t0 t1 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  {t0} {t0} {f'} { nothing } d h fh=gh = begin
-                    FMap Γ f' o nmap t0 d h 
-                ≈⟨⟩
-                   nil {!!}  o h 
-                ≈⟨ nil-idL {!!} ⟩
-                    h 
-                ≈↑⟨ idR  ⟩
+         commute1  {x} {y} {f'}  d h fh=gh with hom f'
+         commute1  {t0} {t0} {f'}  d h fh=gh | nothing = begin
+                    nil none o h
+                ≈⟨ car ( nil-id none ) ⟩
+                    id1 A a o h
+                ≈⟨ idL ⟩
+                    h
+                ≈↑⟨ idR ⟩
                     h o id1 A d
-                ≈⟨⟩
-                    nmap t0 d h o id1 A d
-                ≈⟨⟩
-                    nmap t0 d h o FMap (K A I d) f'
+                ∎
+         commute1  {t0} {t1} {f'}  d h fh=gh | nothing =  begin
+                    nil none o h
+                ≈↑⟨ car ( nil-idL none ) ⟩
+                    (nil none o f ) o h
+                ≈⟨ car ( car ( nil-id none ) ) ⟩
+                    (id1 A b o f ) o h
+                ≈⟨ car idL ⟩
+                    f o h 
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t1} {t0} {f'}  d h fh=gh | nothing =  begin
+                    nil none o ( f o  h )
+                ≈⟨ assoc ⟩
+                    ( nil none o  f ) o h 
+                ≈⟨ car ( nil-idL none ) ⟩
+                     nil none  o h 
+                ≈⟨ car ( nil-id none ) ⟩
+                     id1 A a  o h 
+                ≈⟨ idL ⟩
+                     h 
+                ≈↑⟨ idR ⟩
+                    h o id1 A d
                 ∎
-         commute1  {t0} {t1} {f'} { nothing } d h fh=gh = {!!}
-         commute1  {t1} {t0} {f'} { nothing } d h fh=gh = {!!}
-         commute1  {t1} {t1} {f'} { nothing } d h fh=gh = {!!}
-         commute1  {t1} {t0} {f'} { just inv-f } d h fh=gh = {!!}
-         commute1  {t0} {t1} {f'} { just arrow-f } d h fh=gh =  begin
-                    FMap Γ f' o nmap t0 d h
-                ≈⟨⟩
-                    {!!} o h
-                ≈⟨ {!!} ⟩
+         commute1  {t1} {t1} {f'}  d h fh=gh | nothing =  begin
+                    nil none o  ( f o  h )
+                ≈⟨ car ( nil-id none ) ⟩
+                    id1 A b  o  ( f o  h )
+                ≈⟨ idL ⟩
                      f o  h 
-                ≈↑⟨ idR  ⟩
-                    ( f o  h ) o  id1 A d
-                ≈⟨⟩
-                    nmap t1 d h o FMap (K A I d) f'
+                ≈↑⟨ idR ⟩
+                    ( f o  h ) o id1 A d
+                ∎
+         commute1  {t1} {t0} {f'}  d h fh=gh | just inv-f = begin
+                    nil none o (  f o  h )
+                ≈⟨ assoc ⟩
+                    ( nil none o   f ) o  h 
+                ≈⟨ car ( nil-idL none )  ⟩
+                     nil none  o  h 
+                ≈⟨ car ( nil-id none ) ⟩
+                     id1 A a  o  h 
+                ≈⟨ idL ⟩
+                    h 
+                ≈↑⟨ idR ⟩
+                    h o id1 A d
+                ∎
+         commute1  {t0} {t1} {f'}  d h fh=gh | just arrow-f =  begin
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
                 ∎
-         commute1  {t0} {t1} {f'} { just arrow-g } d h fh=gh =  begin
-                    FMap Γ f' o nmap t0 d h
-                ≈⟨⟩
-                    ? o h
-                ≈⟨ {!!} ⟩
+         commute1  {t0} {t1} {f'}  d h fh=gh | just arrow-g =  begin
+                    g o h
+                ≈↑⟨ fh=gh ⟩
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t0} {t0} {f'}  d h fh=gh | just id-t0 =   begin
+                    id1 A a o h
+                ≈⟨ idL ⟩
+                    h
+                ≈↑⟨ idR ⟩
+                    h o id1 A d
+                ∎
+         commute1  {t1} {t1} {f'}  d h fh=gh | just id-t1 =   begin
+                    id1 A b o  ( f o  h  )
+                ≈⟨ idL ⟩
                      f o  h
-                ≈↑⟨ idR  ⟩
-                    ( f o  h ) o  id1 A d
-                ≈⟨⟩
-                    nmap t1 d h o FMap (K A I d) f'
+                ≈↑⟨ idR ⟩
+                    ( f o  h ) o id1 A d 
                 ∎
-         commute1  {t0} {t0} {f'} { just id-t0 } d h fh=gh = {!!}
-         commute1  {t1} {t1} {f'} { just id-t1 } d h fh=gh = {!!}
          nat1 : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
          nat1 d h fh=gh = record {
             TMap = λ x → nmap x d h ;
             isNTrans = record {
-                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} { hom 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