Mercurial > hg > Members > kono > Proof > category

changeset 963:50d8750d32c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Feb 2021 14:11:12 +0900
parents 9cf91e773517
children 0128a662eb02
files src/CCC.agda src/ToposEx.agda src/equalizer.agda
diffstat 3 files changed, 81 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Mon Feb 22 21:31:38 2021 +0900
+++ b/src/CCC.agda	Tue Feb 23 14:11:12 2021 +0900
@@ -126,17 +126,16 @@
 --
 -- Sub Object Classifier as Topos
 -- pull back on
---                   ○ b
---       b ----------------------→ 1
---       |                         |
---       |                         |
---     m |                         | ⊤
---       |                         |
---       ↓                         ↓
---       a ----------------------→ Ω
---                    h
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+--             h
 --
 open Equalizer
+open import equalizer
 
 record Mono  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set  (c₁ ⊔ c₂ ⊔ ℓ)  where
      field
@@ -144,8 +143,6 @@
 
 open Mono
 
-open import equalizer
-
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
         ( Ω : Obj A )
         ( ⊤ : Hom A １ Ω )
@@ -153,7 +150,7 @@
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          char-ker  : {a b : Obj A } {h : Hom A a Ω} 
-             → A [ char (equalizer (Ker h)) record { isMono = monic (Ker h) } ≈ h ]
+             → A [ char (equalizer (Ker h)) record { isMono = λ f g → monic (Ker h) } ≈ h ]
          ker-char : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → Iso A b (  equalizer-c (Ker ( char m mono ))) 
 
 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -166,10 +163,29 @@
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
 
+record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
+         Nat   : Obj A
+         nzero : Hom A １ Nat
+         nsuc  : Hom A Nat Nat
+
+open NatD
+
+record IsToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (TNat : NatD A １ )
+       (  gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat) )
+  : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
+         izero : (nat : NatD A １ ) → A [ A [ gNat nat o nzero TNat ] ≈ nzero nat ]
+         isuc  : (nat : NatD A １ ) → A [ A [ gNat nat o nsuc TNat ] ≈ A [ nsuc nat o gNat nat ] ]
+
+record ToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １  : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
+         TNat : NatD A １
+         gNat : (nat : NatD A １ ) → Hom A (Nat TNat) (Nat nat)
+         isToposN : IsToposNat A １ TNat gNat
 
 
 
 
 
 
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ToposEx.agda	Tue Feb 23 14:11:12 2021 +0900
@@ -0,0 +1,49 @@
+module ToposEx where
+open import CCC
+open import Level
+open import Category
+open import cat-utility
+open import HomReasoning
+
+open Topos
+open Equalizer
+
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+--             h
+
+
+topos-pullback : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １)
+  → (e2  : {a : Obj A} → ∀ { f : Hom A a １ } →  A [ f ≈ ○ a ] )
+  → (t : Topos A １ ○ ) → {a : Obj A}  → (h : Hom A a (Ω t)) → Pullback A h (⊤ t)
+topos-pullback A １ ○ e2 t {a} h = record {
+     --   Ker t h : Equalizer A h (A [ ⊤ o (○ a) ])
+      ab = equalizer-c (Ker t h)         -- b
+    ; π1 = equalizer   (Ker t h)         -- m
+    ; π2 = ○ ( equalizer-c (Ker t h) )   -- ○ b
+    ; isPullback = record {
+              commute = comm
+         ;    pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (lemma1 p1 p2 eq )
+         ;    π1p=π1 = {!!}
+         ;    π2p=π2 = {!!}
+         ;    uniqueness = {!!}
+      }
+  } where
+    open ≈-Reasoning A
+    comm :  A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ]
+    comm = begin
+            h o equalizer (Ker t h)      ≈⟨ {!!}  ⟩
+            ⊤ t o ○ (equalizer-c (Ker t h))   ∎
+    lemma1 : {d : Obj A}  (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] )
+        → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ]
+    lemma1 {d} p1 p2 eq = begin
+            h o p1                      ≈⟨ eq ⟩
+            ⊤ t o p2                    ≈⟨ cdr e2 ⟩
+            ⊤ t o  (○ d)                ≈↑⟨ cdr e2 ⟩
+            ⊤ t o ( ○ a o p1 )          ≈⟨ assoc ⟩
+           (⊤ t o ○ a ) o p1            ∎ 
+
--- a/src/equalizer.agda	Mon Feb 22 21:31:38 2021 +0900
+++ b/src/equalizer.agda	Tue Feb 23 14:11:12 2021 +0900
@@ -82,10 +82,10 @@
 --        ||
 --         d
 
-monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) 
+monic : { a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g) 
       →  { i j : Hom A d (equalizer-c eqa) }
       →  A [ A [ equalizer eqa o i ]  ≈  A [ equalizer eqa o j ] ] →  A [ i  ≈ j  ]
-monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
+monic {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
                  i
               ≈↑⟨ uniqueness (isEqualizer eqa) ( begin
                    equalizer eqa  o i
@@ -332,7 +332,7 @@
 -- Bourroni equations gives an Equalizer
 --
 
-lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g 
+lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g 
 lemma-equ2 {a} {b} f g bur = record {
       fe=ge = fe=ge1 ;  
       k = k1 ;