Mercurial > hg > Members > kono > Proof > category

changeset 481:65e6906782bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Completeness of Comma Category begin
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 10 Mar 2017 23:57:49 +0900
parents 08f9c8a59ff4
children fd752ad25ac0
files Comma1.agda freyd.agda freyd1.agda
diffstat 3 files changed, 89 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Comma1.agda	Fri Mar 10 18:56:21 2017 +0900
+++ b/Comma1.agda	Fri Mar 10 23:57:49 2017 +0900
@@ -169,3 +169,5 @@
        commute2 :  {a b : Obj A } {f : Hom A a b  } →  
            C [ C [ FMap G ( arrow ( FMap N f)) o tmap1 a  ] ≈ C [ tmap1 b  o FMap F ( arrow ( FMap N f )) ]  ]
        commute2 {a} {b} {f} = comm ( FMap N f )
+
+
--- a/freyd.agda	Fri Mar 10 18:56:21 2017 +0900
+++ b/freyd.agda	Fri Mar 10 23:57:49 2017 +0900
@@ -141,3 +141,5 @@
                  f'
              ∎  )
  
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/freyd1.agda	Fri Mar 10 23:57:49 2017 +0900
@@ -0,0 +1,85 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+
+module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ}  {C : Category c₁' c₂' ℓ'} 
+    ( F : Functor A C ) ( G : Functor A C ) where
+
+open import cat-utility
+open import HomReasoning
+open import Relation.Binary.Core
+open Functor
+
+open import Comma1 F G
+open import freyd CommaCategory
+
+open import Category.Cat
+
+open NTrans
+
+
+tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) 
+     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 
+         ( U : Functor B C)  → NTrans I C ( K C I (FObj U lim) ) (U  ○  Γ)
+tb B I Γ lim tb U = record {
+               TMap  = TMap (Functor*Nat I C U tb) ; 
+               isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (C) in begin
+                     FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a 
+                 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
+                     TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f 
+                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
+                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
+                 ∎
+               } }
+
+open Complete
+
+open CommaObj
+open CommaHom
+open Limit
+
+FIA : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I A
+FIA {I} Γ = record {
+        FObj = λ x → obj (FObj Γ x ) ;
+        FMap = λ {a} {b} f →  arrow (FMap Γ f )  ;
+        isFunctor = record {
+             identity = λ{x} → {!!}
+             ; distr = λ {a} {b} {c} {f} {g}   → {!!} 
+             ; ≈-cong = λ {a} {b} {c} {f}   → {!!}
+          }}
+
+commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  → Obj CommaCategory
+commaLimit {I} comp Γ = record {
+      obj = limit-c  comp (FIA Γ)
+      ; hom = limitHom
+   } where
+       limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
+       limitHom =  C [ FMap G ( limit (isLimit comp (FIA Γ)) {!!} {!!} )   o  {!!}   ]
+
+
+commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
+     → ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ )
+     → NTrans I CommaCategory (K CommaCategory I (commaLimit comp Γ)) Γ
+commaNat {I} comp  Γ ta = record {
+       TMap = λ x → tmap x
+       ; isNTrans = record { commute = {!!} }
+    } where
+        tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I (commaLimit comp Γ)) i) (FObj Γ i)
+        tmap i = record {
+              arrow = A [ {!!} o  limit ( isLimit comp (FIA Γ ) ) {!!} {!!} ]
+              ; comm = {!!}
+          }
+        commute : {a b : Obj I} {f : Hom I a b} → 
+              CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I (commaLimit comp Γ)) f ] ]
+        commute {a} {b} {f} = {!!}
+
+
+hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
+    → ( G-preserve-limit :  ( Γ : Functor I A ) 
+       ( lim : Obj A ) ( ta : NTrans I A ( K A I lim ) Γ ) → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G  ) )
+    → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ ) 
+    → Limit CommaCategory I Γ (commaLimit comp Γ ) ( commaNat comp  Γ ta ) 
+hasLimit {I} comp gpresrve Γ ta  = record {
+     limit = λ a t → {!!} ;
+     t0f=t = λ {a t i } →  {!!} ;
+     limit-uniqueness =  λ {a} {t} f t=f →  {!!}
+   }