Mercurial > hg > Members > kono > Proof > category

changeset 608:7194ba55df56

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
freyd2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Jun 2017 10:50:02 +0900
parents caab94e897e6
children d686d7ae38e0
files S.agda SetsCompleteness.agda freyd.agda freyd2.agda
diffstat 4 files changed, 117 insertions(+), 53 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/S.agda	Mon Jun 12 10:50:02 2017 +0900
@@ -0,0 +1,49 @@
+--I'd like to write the Limit in Sets Category using Agda. Assuming local smallness, a functor is a pair of map on Set OC and I, like this.
+--
+--     sobj :  OC →  Set  c₂
+--     smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j
+--
+--A cone for the functor is a record with two fields. Using the record, commutativity of the cone and the propertiesy of the Limit
+--are easity shown, except uniquness. The uniquness of the Limit turned out that congruence of the record with two fields.
+--
+--In the following agda code, I'd like to prove snat-cong lemma.
+
+    open import Level
+    module S where
+
+    open import Relation.Binary.Core
+    open import Function
+    import Relation.Binary.PropositionalEquality
+
+    record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
+         ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
+       field
+           snmap : ( i : OC ) → sobj i
+           sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
+       smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
+       smap0 {i} {j} f x =  smap f x
+
+    open snat
+
+    snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
+             ( s t :  snat SObj SMap   )
+         → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
+         → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
+         → s ≡ t
+    snat-cong s t refl refl = {!!}
+
+--This is quite simlar to the answer of 
+--
+--    Equality on dependent record types
+--    https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types
+--
+--So it should work something like
+--
+--    snat-cong s t refl refl = refl
+--
+--but it gives an error like this.
+--
+--    .sncommute i j f != sncommute t i j f of type
+--    .SMap f (snmap t i) ≡ snmap t j
+--
+--Is there any help?
--- a/SetsCompleteness.agda	Thu Jun 08 19:48:02 2017 +0900
+++ b/SetsCompleteness.agda	Mon Jun 12 10:50:02 2017 +0900
@@ -175,10 +175,18 @@
 
 open snat
 
+≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C )
+    →  a  ≡  a'
+    →  b  ≡  b'
+    →  f a b  ≡  f a' b'
+≡cong2 _ refl refl = refl
+
+open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
+
 snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
          ( s t :  snat SObj SMap   )
      → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
-     → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡  (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
+     → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
      → s ≡ t
 snat-cong s t refl refl = {!!}
 
@@ -238,7 +246,7 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
-             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq2 x )  ⟩
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) {!!}  ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j f' → sncommute (f x ) i j f'  }
              ≡⟨⟩
                   f x
--- a/freyd.agda	Thu Jun 08 19:48:02 2017 +0900
+++ b/freyd.agda	Mon Jun 12 10:50:02 2017 +0900
@@ -1,7 +1,7 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+module freyd {c₁ c₂ ℓ : Level} 
   where
 
 open import cat-utility
--- a/freyd2.agda	Thu Jun 08 19:48:02 2017 +0900
+++ b/freyd2.agda	Mon Jun 12 10:50:02 2017 +0900
@@ -18,6 +18,20 @@
 --
 
 -- A is Locally small
+
+----
+-- 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
+
+
 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
 
 import Relation.Binary.PropositionalEquality
@@ -66,7 +80,6 @@
              ∎ )
 
 
--- {*}↓U has preinitial full subcategory iff U is representable
 
 record Representable  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set  (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ ))  where
    field
@@ -77,56 +90,50 @@
 
          repr→ : NTrans A (Sets {c₂}) U (HomA A b )
          repr← : NTrans A (Sets {c₂}) (HomA A b)  U
-         representable→  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
-         representable←  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+         reprId  :  {x : Obj A} →  Sets [ Sets [ TMap repr→ x  o  TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )]
+         reprId  :  {x : Obj A} →  Sets [ Sets [ TMap repr← x  o  TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)]
+
+open import freyd
 
--- HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →  (b : Obj A)
---       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
---       → LimitPreserve A I (Sets  {c₂}) ( HomA A b )
--- HpreseveLimit {_} { c₂} A b I =  record {
---        preserve = λ Γ limita → record {
---              limit = λ a t → limitu a Γ t limita
---              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
---              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
---        }
---    } where
---       limitu :   ( a : Obj Sets ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
---           Hom Sets a (FObj (HomA A b) (a0 limita))
---       limitu  = {!!}
---       t0f=tu :    { a : Obj  Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
---            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ]
---       t0f=tu  = {!!}
---       limit-uniquenessu :    { a : Obj Sets } → (Γ : Functor I A ) 
---            →   ( limita : Limit A I Γ  ) →
---           ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f :  Hom Sets a (FObj (HomA A b) (a0 limita)) ) 
---            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) )
---            →  Sets [ limitu a Γ t limita ≈ f ]
---       limit-uniquenessu = {!!}
+_↓_ :  { 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
 
---
--- 
--- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
---       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
---      ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
--- UpreseveLimit {_} { c₂} A U b I rep =  record {
---        preserve = λ Γ limita → record {
---              limit = λ a t → limitu a Γ t limita
---              ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
---              ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
---        }
---    } where
---       limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   
---           Hom Sets a (FObj U (a0 limita))
---       limitu  = {!!}
---       t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
---            ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
---       t0f=tu  = {!!}
---       limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
---            →   ( limita : Limit A I Γ  ) →
---           ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
---            →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
---            →  Sets [ limitu a Γ t limita ≈ f ]
---       limit-uniquenessu = {!!}
--- 
+-- K{*}↓U has preinitial full subcategory then U is representable
+
+open SmallFullSubcategory
+open Complete
+open PreInitial
+
+data OneObject : Set where
+  * : OneObject
+
+UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+      (comp : Complete A A)
+      (U : Functor A (Sets) )
+      (SFS : SmallFullSubcategory ( K (Sets) {!!} {!!} ↓ U )) → 
+      (PI : PreInitial {!!} (SFSF SFS )) → Representable A U {!!}
+UisRepresentable = {!!}
+
+-- K{*}↓U has preinitial full subcategory if U is representable
+
+KUhasSFS : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+      (comp : Complete A A)
+      (U : Functor A (Sets) )
+      (a : Obj A )
+      (R : Representable A U a ) →
+      SmallFullSubcategory {!!}
+KUhasSFS = {!!}
+
+KUhasPreinitial : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+      (comp : Complete A A)
+      (U : Functor A (Sets) )
+      (a : Obj A )
+      (R : Representable A U a ) →
+      PreInitial {!!} (SFSF (KUhasSFS A comp U a R ) )
+KUhasPreinitial = {!!}