Mercurial > hg > Members > kono > Proof > category

changeset 627:efa1f2103a83

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 Sun, 25 Jun 2017 13:03:33 +0900
parents c5abbd39e6eb
children b99660fa14e1
files freyd2.agda
diffstat 1 files changed, 10 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Sat Jun 24 08:34:36 2017 +0900
+++ b/freyd2.agda	Sun Jun 25 13:03:33 2017 +0900
@@ -17,18 +17,6 @@
 --    U ⋍ Hom (a,-)
 --
 
-----
--- C is locally small i.e. Hom C i j is a set c₁
---
-record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
-                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-   field
-     hom→ : {i j : Obj C } →    Hom C i j →  I
-     hom← : {i j : Obj C } →  ( f : I ) →  Hom C i j
-     hom-iso : {i j : Obj C } →  { f : Hom C i j } →   hom← ( hom→ f )  ≡ f
-
-open Small
-
 -- maybe this is a part of local smallness
 postulate ≈-≡ :  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
 
@@ -186,14 +174,15 @@
        preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim
    } 
 
-data * {c : Level} : Set c where
-  OneObj : *
 
 -- K{*}↓U has preinitial full subcategory if U is representable
 --     if U is representable,  K{*}↓U has initial Object ( so it has preinitial full subcategory )
 
 open CommaHom
 
+data * {c : Level} : Set c where
+  OneObj : *
+
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
       → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
@@ -258,45 +247,27 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
 
-isRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+UisRepresentable : {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 = {!!} } }
+UisRepresentable A U SFS PI = record {
+        repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
         ; reprId→  = λ {y}  →　?
         ; reprId←  = λ {y}  →　?
    } where
+      ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
+      ub b x OneObj = x
       tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj (preinitialObj PI))) b)
-      tmap1 b x = arrow ( SFSFMap← SFS ( preinitialArrow PI ) )
+      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 ) →