Mercurial > hg > Members > kono > Proof > category

changeset 496:5c7908202d5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2017 13:37:07 +0900
parents 633df882db86
children e8b85a05a6b2
files freyd1.agda
diffstat 1 files changed, 4 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/freyd1.agda	Tue Mar 14 13:08:03 2017 +0900
+++ b/freyd1.agda	Tue Mar 14 13:37:07 2017 +0900
@@ -48,16 +48,6 @@
              id1 A  (obj (FObj Γ x))     
          ∎
 
-Γa : { I : Category c₁ c₂ ℓ } →  ( a : Obj A)  → Functor I A
-Γa  a = record {
-  FObj = λ x → a ;
-  FMap = λ {x} {y} f →  id1 A a  ;
-  isFunctor = record {
-             identity = let  open ≈-Reasoning (A) in refl-hom
-             ; distr = let  open ≈-Reasoning (A) in sym ( idL )
-             ; ≈-cong =  λ _ → let  open ≈-Reasoning (A) in refl-hom
-          }} where
-
 --- Get a nat on A from a nat on CommaCategory
 --
 NIA : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
@@ -81,9 +71,6 @@
     → Limit C I (G  ○  (FIA Γ)) 
 LimitC  {I} comp Γ glimit  = plimit glimit (climit comp (FIA Γ))
 
-frev :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory ) (i : Obj I ) → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
-frev comp Γ i = TMap (t0 ( climit comp (FIA Γ)))  i
-
 tu :  { I : Category c₁ c₂ ℓ } →  ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
     →   NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G  ○  (FIA Γ))
 tu {I} comp Γ = record {
@@ -91,10 +78,10 @@
     ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
   } where
         commute : {a b : Obj I} {f : Hom I a b}   →
-              C [ C [ FMap (G  ○  (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (frev comp Γ a) ] ] 
-            ≈ C [ C [ hom (FObj Γ b) o FMap F (frev comp Γ b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
+              C [ C [ FMap (G  ○  (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ] 
+            ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
         commute  {a} {b} {f} =  let  open ≈-Reasoning (C) in begin
-             FMap (G  ○  (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (frev comp Γ a) )
+             FMap (G  ○  (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ)))  a ))
          ≈⟨⟩
              FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ))
          ≈⟨ assoc ⟩
@@ -116,7 +103,7 @@
          ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩
               hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ))))
          ≈⟨ assoc ⟩
-             ( hom (FObj Γ b) o FMap F (frev comp Γ b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f
+             ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f
          ∎
 limitHom :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory )
     → ( glimit :  LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
@@ -203,8 +190,6 @@
        arrow  = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
      ; comm = comm1
    } where
-      tcomm : { x y : Obj I } { f : Hom I x y} → A [ A [ FMap (FIA Γ) f  o  TMap (NIA Γ a t) x ] ≈ A [ TMap (NIA  Γ a t) y o id1 A (obj a) ] ]
-      tcomm  {x} {y} {f} = ( IsNTrans.commute ( isNTrans t )) {x} {y} {f}
       comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ]
         ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ]
       comm1 =  let  open ≈-Reasoning (C) in begin