Mercurial > hg > Members > kono > Proof > category

changeset 1097:321f0fef54c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Todo
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Jul 2021 06:58:48 +0900
parents f6d976d26c5a
children 0484477868fe 56c88ca85d07
files Todo.md src/CCC.agda src/yoneda.agda
diffstat 3 files changed, 78 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Todo.md	Sat Jul 31 06:58:48 2021 +0900
@@ -0,0 +1,50 @@
+Todo
+====
+
+CCCGraph.agda            
+---
+CCC generated from Graph (iconmplete) p.55
+
+   cat-graph-univ :  {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (CAT {c₁ } {c₁} {c₁}) forgetful.UC 
+   ccc-graph-univ :  {c₁ : Level} → UniversalMapping (Grph {c₁} {c₁}) (Cart {c₁ } {c₁} {c₁}) forgetful.UX 
+
+Polynominal.agda         
+---
+Polynominal Category and functional completeness
+
+  -- an assuption needed in k x phi ≈ k x phi'
+  --   k x (i x) ≈ k x ii  
+  postulate 
+       xf :  {a b c : Obj A } → ( x : Hom A １ a ) → {z : Hom A b c } → ( y  : φ {a} x z ) → ( x ∙ π' ) ≈ π 
+
+  define Polynominal Category as a graph generated one
+  define Polynominal Category as a coMonad
+
+Topos
+---
+
+   ToposEx.agda             Topos Exercise (incomplete)                p.141
+   ToposIL.agda             Topos Internal Language (incomplete)       p.143
+   ToposSub.agda            Topos Subobject classifier (incomplete)
+
+equalizer.agda           
+---
+Equalizer example p.21
+
+Bourroni equations gives an Equalizer
+
+   postulate 
+     uniqueness1 : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } →
+        A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq  ≈ k' ]
+
+system-f.agda
+---
+
+   very incomplete, because this is a meta circular interpreter of Agda
+
+yoneda.agda              
+---
+Yoneda Functor p.11
+
+     ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b
+
--- a/src/CCC.agda	Wed May 19 09:00:25 2021 +0900
+++ b/src/CCC.agda	Sat Jul 31 06:58:48 2021 +0900
@@ -230,14 +230,19 @@
 -- Sub Object Classifier as Topos
 -- pull back on
 --
+--  m ∙ f ≈ m ∙ g → f ≈ g
+--
 --     iso          ○ b
---  e ⇐====⇒  b -----------→ 1         m ∙ f ≈ m ∙ g → f ≈ g
+--  e ⇐====⇒  b -----------→ 1 
 --  |         |              |
 --  |       m |              | ⊤
---  |         ↓    char m    ↓    Ker h = Equalizer (char m mono)  (⊤ ∙ ○ a )
---  + ------→ a -----------→ Ω        m = Equalizer (char m mono)  (⊤ ∙ ○ a )
+--  |         ↓    char m    ↓    
+--  + ------→ a -----------→ Ω  
 --     ker h        h
 --
+--     Ker h = Equalizer (char m mono)  (⊤ ∙ ○ a )
+--     m = Equalizer (char m mono)  (⊤ ∙ ○ a )
+--
 --  if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer.
 --    equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g )
 --      → (m :  Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g
@@ -251,10 +256,9 @@
          ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
          char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
              → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
-         -- char-iso :  {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) →
-         --        Iso A a a'  → A [ char p mp  ≈ char q mq ]
          char-iso :  {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) →
                 (i : Iso A a a' ) → A [ p ≈ A [ q o Iso.≅→ i ] ]  → A [ char p mp  ≈ char q mq ]
+         -- this means, char m is unique among all equalizers of h and ○  a
      char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
              → A [ m  ≈  m'  ] → A [ char m mono ≈ char m' mono'  ]
      char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) ( begin 
--- a/src/yoneda.agda	Wed May 19 09:00:25 2021 +0900
+++ b/src/yoneda.agda	Sat Jul 31 06:58:48 2021 +0900
@@ -15,9 +15,7 @@
 open import HomReasoning
 open import Relation.Binary.Core
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
-
-
+open import Relation.Binary.PropositionalEquality hiding ( [_] ; resp ) renaming ( sym to ≡sym )
 
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
 --   Obj and Hom of Sets^A^op
@@ -386,14 +384,27 @@
 --- How to prove it? from smallness?
 
 data _~_   {a b : Obj A} (f : Hom A a b)
-     : ∀{x y : Obj A} → Hom A x y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
-  refl : {g : Hom A a b} → (eqv : A [ f ≈ g ]) →  f ~ g
+      : ∀{x y : Obj A} → Hom A x y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+   ~refl : {g : Hom A a b} → (eqv : A [ f ≈ g ]) →  f ~ g
+
+≃→b=b : {a b a' b' : Obj A }
+      → ( f : Hom A a b )
+      → ( g : Hom A a' b' )
+      → f ~ g → b ≡ b'
+≃→b=b f g (~refl eqv) = refl
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 postulate  -- ?
-     eqObj1 : {a b a' b' : Obj A } → Hom A a b ≡ Hom A a' b' → b ≡ b'
+     ylem0 : {a b : Obj A } → Hom A a a ≡ Hom A a b → a ≡ b
 
 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
-Yoneda-full-embed {a} {b} eq = eqObj1 ylem1 where
+Yoneda-full-embed {a} {b} eq = ylem0 ylem1 where
      ylem1 : Hom A a a ≡ Hom A a b
      ylem1 = cong (λ k → FObj k a) eq
-
+     f : Hom A a b
+     f = subst (λ k → k ) ylem1 (id1 A a)
+     -- f1 : id1 A a ≅ f
+     -- f1 = {!!}
+     -- f2 : id1 A a ≅ f → Category.cod A (id1 A a) ≡  Category.cod A f
+     -- f2 = {!!}