Mercurial > hg > Members > kono > Proof > category

changeset 626:c5abbd39e6eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 24 Jun 2017 08:34:36 +0900
parents d73fbed639a9
children efa1f2103a83
files freyd2.agda
diffstat 1 files changed, 67 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Fri Jun 23 21:43:09 2017 +0900
+++ b/freyd2.agda	Sat Jun 24 08:34:36 2017 +0900
@@ -255,20 +255,70 @@
 
 open SmallFullSubcategory
 open PreInitial
---  
--- UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
---       (U : Functor A (Sets {c₂}) )
---       (a : Obj (Sets {c₂})) (ax : a)
---       (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) )  
---       (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) 
---         → Representable A U (obj (preinitialObj PI ))
--- UisRepresentable A U a ax SFS PI = record {
---          repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }
---          ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = {!!} } }
---          ; reprId→  = λ {y}  →　?
---          ; reprId←  = λ {y}  →　?
---     } where
---        tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
---        tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
---        tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
---        tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) ax )
+
+≡-cong = Relation.Binary.PropositionalEquality.cong
+
+isRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+     (U : Functor A (Sets {c₂}) )
+     (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A * ↓ U) )  
+     (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A * ↓ U) (SFSF SFS )) 
+       → Representable A U (obj (preinitialObj PI ))
+isRepresentable A U SFS PI = record {
+        repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }
+        ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
+        ; reprId→  = λ {y}  →　?
+        ; reprId←  = λ {y}  →　?
+   } where
+      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
+      tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
+      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
+      tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
+      comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
+          ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )] ) y
+             ≡ ( Sets [( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f  ] ) y 
+      comm11 a b f y =  begin
+                ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )] ) y
+             ≡⟨⟩
+                ( FMap (Yoneda A (obj (preinitialObj PI))) f ) ( arrow ( SFSFMap← SFS ( preinitialArrow PI )))
+             ≡⟨⟩
+                A [ f o ( arrow ( SFSFMap← SFS ( preinitialArrow PI ))) ]
+             ≡⟨ {!!} ⟩
+                arrow ( SFSFMap← SFS ( preinitialArrow PI ))
+             ≡⟨⟩
+                ( Sets [( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f  ] ) y 
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+      comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ]
+      comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
+                FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 
+             ≈⟨⟩
+                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) )
+             ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
+                ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI ) ) ) o FMap U f 
+             ≈⟨⟩
+                tmap1 b o FMap U f 
+             ∎ 
+      comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj (preinitialObj PI)) a ) → 
+          (Sets [ FMap U f o (λ x → FMap U x (hom (preinitialObj PI) OneObj))] ) y ≡
+                (Sets [ ( λ x → (FMap U x ) (hom (preinitialObj PI) OneObj)) o (λ x → A [ f o x ] ) ] )  y
+      comm21 a b f y = begin
+                FMap U f ( FMap U y (hom (preinitialObj PI) OneObj))
+             ≡⟨ ≡-cong ( λ k → k (hom (preinitialObj PI) OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩
+                (FMap U (A [ f o y ] ) ) (hom (preinitialObj PI) OneObj) 
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+      comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
+        Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
+      comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin
+                FMap U f o tmap2 a 
+             ≈⟨⟩
+                FMap U f o ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) )
+             ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩
+                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o ( λ x → A [ f o x  ]  )
+             ≈⟨⟩
+                ( λ x → ( FMap U x ) ( hom ( preinitialObj PI ) OneObj ) ) o FMap (Yoneda A (obj (preinitialObj PI))) f 
+             ≈⟨⟩
+                tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f 
+             ∎