Mercurial > hg > Members > kono > Proof > category

changeset 632:d36ff598a063

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add compleness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 27 Jun 2017 10:29:06 +0900
parents 7be3eb96310c
children 37fa9d3fab8c
files freyd.agda freyd2.agda
diffstat 2 files changed, 32 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/freyd.agda	Mon Jun 26 21:58:55 2017 +0900
+++ b/freyd.agda	Tue Jun 27 10:29:06 2017 +0900
@@ -16,6 +16,7 @@
       SFSF : Functor A A  
       SFSFMap← : { a b : Obj A } → Hom A (FObj SFSF a) (FObj SFSF b ) → Hom A a b 
       full→ : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ FMap SFSF ( SFSFMap← x ) ≈ x ]
+      full← : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ SFSFMap← ( FMap SFSF x ) ≈ x ]
 
       -- ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj SFSF a) (FObj SFSF b) } → 
       --          (x≈y : A [ FMap SFSF x ≈ FMap SFSF y  ]) → FMap SFSF x ≡ FMap SFSF y   -- codomain of FMap is local small
--- a/freyd2.agda	Mon Jun 26 21:58:55 2017 +0900
+++ b/freyd2.agda	Tue Jun 27 10:29:06 2017 +0900
@@ -247,13 +247,12 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong
 
-
-UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( comp : Complete A A )
      (U : Functor A (Sets {c₂}) )
      (SFS : SmallFullSubcategory ( K (Sets {c₂}) A * ↓ U) )  
      (PI : PreInitial ( K (Sets) A * ↓ U)  (SFSF SFS)) 
        → Representable A U (obj (preinitialObj PI ))
-UisRepresentable A U SFS PI = record {
+UisRepresentable A comp U SFS PI = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
         ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } }
         ; reprId→  = {!!}
@@ -270,15 +269,7 @@
       piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b
       piArrow b =  SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} )
       fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
-      fArrowComm1 a b f x OneObj = begin
-               FMap U f ( ub a x OneObj ) 
-             ≡⟨⟩
-               FMap U f x
-             ≡⟨⟩
-               ub b (FMap U f x) OneObj
-             ∎  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+      fArrowComm1 a b f x OneObj = refl
       fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
          Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
       fArrowComm a b f x = extensionality Sets ( λ y → begin 
@@ -298,11 +289,31 @@
                   open ≡-Reasoning
       fArrow :  (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
       fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x }
-      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
-      tmap1 b x =  arrow ( piArrow ( ob b x ) )
       preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ]
          ≈ Sets [ ub a x  o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ]
       preinitComm a x = comm (piArrow (ob a x ))
+      comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b )  → ( K Sets A * ↓ U) [
+           ( K Sets A * ↓ U) [ f o preinitialArrow PI ]  ≈ preinitialArrow PI ]   
+      comm13 a b f = let open ≈-Reasoning A in begin
+                arrow ( ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ) 
+             ≈⟨⟩
+                arrow f o arrow ( preinitialArrow PI )
+             ≈⟨ {!!} ⟩
+                arrow ( preinitialArrow PI  )
+             ∎ 
+      comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [
+          FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ] 
+      comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin
+                FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) 
+             ≈⟨ {!!} ⟩
+                FMap (SFSF SFS) ( fArrow a b f y ) o FMap (SFSF SFS) ( piArrow (ob a y)) 
+             ≈⟨ {!!} ⟩
+                FMap (SFSF SFS) ( fArrow a b f y ) o preinitialArrow PI {FObj (SFSF SFS) (ob a y ) }
+             ≈⟨ comm13 (FObj (SFSF SFS) (ob a y)) (FObj (SFSF SFS) (ob b (FMap U f y))) (FMap (SFSF SFS) (fArrow a b f y)) ⟩
+                preinitialArrow PI {FObj (SFSF SFS) (ob b (FMap U f y )) }
+             ≈⟨ {!!} ⟩
+                FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) 
+             ∎ 
       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 (piArrow (ob a x))) ] ) y   
            ≡ (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
@@ -315,12 +326,18 @@
              ≡⟨⟩
                 arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] )
              ≡⟨ {!!} ⟩
+                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] ) ) )
+             ≡⟨ ≡-cong ( λ k → arrow ( (SFSFMap← SFS ) k ))  ( ≈-≡ ( K Sets A * ↓ U) ( comm12 a b f y ) ) ⟩
+                arrow ( ( SFSFMap← SFS ) (  FMap (SFSF SFS) ( piArrow (ob b (FMap U f y) ) )) )
+             ≡⟨ {!!} ⟩
                 arrow (piArrow (ob b (FMap U f y) ))
              ≡⟨⟩
                 (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
+      tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
+      tmap1 b x =  arrow ( piArrow ( ob b x ) )
       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