Mercurial > hg > Members > kono > Proof > category

changeset 624:9b9bc1e076f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introduce one element set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Jun 2017 21:20:10 +0900
parents bed3be9a4168
children d73fbed639a9
files freyd2.agda
diffstat 1 files changed, 69 insertions(+), 84 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Fri Jun 23 19:11:36 2017 +0900
+++ b/freyd2.agda	Fri Jun 23 21:20:10 2017 +0900
@@ -17,6 +17,18 @@
 --    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
 
@@ -24,6 +36,7 @@
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
+
 ----
 --
 --  Hom ( a, - ) is Object mapping in Yoneda Functor
@@ -81,6 +94,19 @@
 open Representable
 open import freyd
 
+_↓_ :  { c₁ c₂ ℓ : Level}  { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' }
+    →  ( F G : Functor A B )
+    →  Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
+_↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'}  { A } { B } F G  = CommaCategory
+         where open import Comma1 F G
+
+open import freyd
+open SmallFullSubcategory
+open Complete
+open PreInitial
+open HasInitialObject
+open import Comma1
+open CommaObj
 open LimitPreserve
 
 -- Representable Functor U preserve limit , so K{*}↓U is complete
@@ -160,103 +186,62 @@
        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 )
 
-data OneObject {c : Level} : Set c where
-  OneObj : OneObject
-
-data OneMor {c : Level} : OneObject {c} → OneObject {c} → Set c where
-  OneIdMor : OneMor OneObj OneObj
-
-comp : {A B C : OneObject} → OneMor B C → OneMor A B → OneMor A C 
-comp OneIdMor OneIdMor = OneIdMor
-
-OneEquiv : {c : Level} {A B : OneObject {c} } → IsEquivalence {c} {c} {OneMor A B} _≡_
-OneEquiv = record { refl = refl  ; sym = ≡-sym; trans = ≡-trans}
-
-OneID : {A : OneObject} → OneMor A A
-OneID {OneObj} = OneIdMor
-
-OneAssoc : {A B C D : OneObject} {f : OneMor C D} {g : OneMor B C } {h : OneMor A B}
-           → comp f (comp g h) ≡ comp (comp f g) h 
-OneAssoc {OneObj} {OneObj} {OneObj} {OneObj} {OneIdMor} {OneIdMor} {OneIdMor} = refl
-
-OneIdentityL : {A B : OneObject} {f : OneMor A B} → (comp OneID f) ≡ f
-OneIdentityL {OneObj} {OneObj} {OneIdMor} = refl 
-
-OneIdentityR : {A B : OneObject} {f : OneMor A B} → (comp f OneID) ≡ f
-OneIdentityR {OneObj} {OneObj} {OneIdMor} = refl 
-
-o-resp-≡ : {A B C : OneObject} {f g : OneMor A B} {h i : OneMor B C} → f ≡ g → h ≡ i → comp h f ≡ comp i g
-o-resp-≡ {OneObj} {OneObj} {OneObj} {f} {g} {h} {i} f≡g h≡i =
-  ≡-trans (cong (comp h) f≡g) (cong (λ x → comp x g) h≡i)
-
-
-isCategory : { c : Level } → IsCategory {c} {c} {c} OneObject OneMor _≡_ comp OneID
-isCategory = record { isEquivalence = OneEquiv
-                    ; identityL = OneIdentityL
-                    ; identityR = OneIdentityR
-                    ; o-resp-≈ = o-resp-≡
-                    ; associative = OneAssoc
-                    }
-
-ONE : { c : Level } → Category c c c
-ONE = record { Obj = OneObject
-             ; Hom = OneMor
-             ; _≈_ = _≡_ 
-             ; Id  = OneID
-             ; isCategory = isCategory
-             }
-
-_↓_ :  { c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } { C : Category c₁'' c₂'' ℓ'' }
-    →  ( F : Functor A C )
-    →  ( G : Functor B C )
-    →  Category  (c₂'' ⊔ c₁ ⊔ c₁') (ℓ'' ⊔ c₂ ⊔ c₂') ( ℓ ⊔ ℓ' )
-_↓_   { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {c₁''} {c₂''} {ℓ''} {A} {B} {C} F G  = CommaCategory
-         where open import Comma F G
-
-open import freyd
-open SmallFullSubcategory
-open Complete
-open PreInitial
-open HasInitialObject
-open import Comma
-open CommaObj
 open CommaHom
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → HasInitialObject {c₁} {c₂} {ℓ}  ( K Sets ONE OneObject ↓ (Yoneda A a) ) ( record  { obj = OneObj ; hom = {!!} } )
+      → HasInitialObject {c₁} {c₂} {ℓ}  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
-         ; uniqueness =  {!!}
+         ; uniqueness =  λ b f → unique b f
      } where
          commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
-         commaCat = K Sets ONE OneObject ↓ Yoneda A a
-         initObj  : Obj (K Sets ONE OneObject ↓ Yoneda A a)
-         initObj = record { obj = OneObj ; hom = {!!} }
-         initial0comm1 :  (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → (x :  {!!} )
-            →  FMap (Yoneda A a) (hom b {!!}) x ≡ hom b {!!}
-         initial0comm1 b x =  let open ≈-Reasoning A in ≈-≡ A ( begin
-               FMap (Yoneda A a) (hom b {!!}) x  
+         commaCat = K Sets A * ↓ Yoneda A a
+         initObj  : Obj (K Sets A * ↓ Yoneda A a)
+         initObj = record { obj = a ; hom = λ x → id1 A a }
+         comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] )  x ≡ hom b x
+         comm2 b OneObj = let open ≈-Reasoning A in  ≈-≡ A ( begin
+                ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj
+             ≈⟨⟩
+                FMap (Yoneda A a) (hom b OneObj) (id1 A a)
+             ≈⟨⟩
+                hom b OneObj o id1 A a
+             ≈⟨ idR ⟩
+                hom b OneObj 
+             ∎  )
+         comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ]
+         comm1 b = let open ≈-Reasoning Sets in begin
+                FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a )
+             ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩
+                hom b 
              ≈⟨⟩
-               hom b {!!} o x
-             ≈⟨ {!!} ⟩
-               hom b {!!}
-             ∎ )
-         initial0comm :  (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
-            Sets [ Sets [ FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) ] ≈ {!!} ]
-         initial0comm b = let open ≈-Reasoning Sets in begin
-                   FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) 
-             ≈⟨ {!!} ⟩
-                    {!!}
+                hom b o FMap (K Sets A *) (hom b OneObj) 
              ∎ 
-         initial0 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) →
-            Hom (K Sets ONE OneObject ↓ (Yoneda A a)) initObj b
+         initial0 : (b : Obj commaCat) →
+            Hom commaCat initObj b
          initial0 b = record {
-                arrow = {!!}
-              ; comm = {!!} }
+                arrow = hom b OneObj
+              ; comm = comm1 b }
+         unique : (b : Obj (K Sets A * ↓ Yoneda A a))  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
+                → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
+         unique b f = let open ≈-Reasoning A in begin
+                arrow f
+             ≈↑⟨ idR ⟩
+                arrow f o id1 A a
+             ≈⟨⟩
+                ( Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a)  ] ) (id1 A a)
+             ≈⟨ ≡-≈ ? ⟩
+               ( Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ) OneObj
+             ≈⟨⟩
+                hom b OneObj
+             ∎ 
+
             
 
 -- K{*}↓U has preinitial full subcategory then U is representable
@@ -268,7 +253,7 @@
 --       (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 ONE OneObject ↓ U) (SFSF SFS )) 
+--       (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 = {!!} } }