Mercurial > hg > Members > kono > Proof > category

changeset 494:ba6a67523523

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unique direction 2 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2017 12:14:57 +0900
parents de9ce7e0d97c
children 633df882db86
files freyd1.agda
diffstat 1 files changed, 28 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/freyd1.agda	Tue Mar 14 11:43:46 2017 +0900
+++ b/freyd1.agda	Tue Mar 14 12:14:57 2017 +0900
@@ -170,9 +170,32 @@
      → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → 
               NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ)
 gnat {I} comp Γ glimit a t = record {
-       TMap = ?
-      ; isNTrans = record { commute = ? }
-    }
+       TMap = λ i → C [  hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ]
+      ; isNTrans = record { commute = λ {x y f} → comm1 x y f }
+    } where
+       comm1 :  (x y : Obj I) (f : Hom I x y ) →
+                C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ]
+                ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K C I (FObj F (obj a))) f ] ]
+       comm1 x y f =  let  open ≈-Reasoning (C) in begin
+             FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x  ))
+         ≈⟨⟩
+             FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x  ))
+         ≈⟨ assoc ⟩
+             (FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x))) o FMap F (TMap (NIA Γ a t) x  )
+         ≈⟨ car ( comm (FMap Γ f) ) ⟩
+             ( hom (FObj Γ y)  o  FMap F (FMap (FIA Γ) f )) o FMap F (TMap (NIA Γ a t) x  )
+         ≈↑⟨ assoc ⟩
+              hom (FObj Γ y)  o  ( FMap F (FMap (FIA Γ) f ) o FMap F (TMap (NIA Γ a t) x  ))
+         ≈↑⟨ cdr (distr F) ⟩
+              hom (FObj Γ y)  o  ( FMap F ( A [ FMap (FIA Γ) f  o TMap (NIA Γ a t) x  ])  )
+         ≈⟨ cdr ( fcong F ( IsNTrans.commute ( isNTrans ( NIA Γ a t )))) ⟩
+              hom (FObj Γ y)  o  ( FMap F ( A [ TMap (NIA Γ a t) y   o id1 A (obj a) ])  )
+         ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A)))  ⟩
+              hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y)  
+         ≈↑⟨ idR ⟩
+             ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K C I (FObj F (obj a))) f
+         ∎
+
 
 comma-a0 :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
      → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
@@ -187,7 +210,7 @@
       comm1 =  let  open ≈-Reasoning (C) in begin
             FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a 
          ≈⟨ {!!} ⟩
-            limit (isLimit (LimitC comp Γ glimit  )) (FObj F (obj a)) {!!}
+            limit (isLimit (LimitC comp Γ glimit  )) (FObj F (obj a)) (gnat comp Γ glimit a t )
          ≈⟨ limit-uniqueness  (isLimit (LimitC comp Γ glimit  )) 
              (limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  
                 o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
@@ -211,7 +234,7 @@
                            hom ( FObj Γ i ) o  
                                FMap F ( A [ TMap (t0 ( climit comp (FIA Γ)))  i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] )
                    ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ 
-                           hom ( FObj Γ i ) o FMap F ( TMap {!!} i )
+                           hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i )
                    ≈⟨ {!!} ⟩ 
                        TMap {!!} i
                  ∎