changeset 973:5f76e5cf3d49

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Feb 2021 17:31:13 +0900
parents e05eb6029b5b
children 5731ffd6cf7a
files src/CCC.agda src/ToposEx.agda
diffstat 2 files changed, 24 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Sat Feb 27 22:57:42 2021 +0900
+++ b/src/CCC.agda	Sun Feb 28 17:31:13 2021 +0900
@@ -169,8 +169,8 @@
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]))
         (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 = λ f g → monic (Ker h) } ≈ h ]
+         char-ker  : {a b : Obj A }  (m : Hom A b a ) → ( mono : Mono A m ) → {h : Hom A a Ω}
+             → A [ char m mono  ≈ 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₂ ℓ)  ( 1 : Obj A) (○ : (a : Obj A ) → Hom A a 1) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -182,6 +182,8 @@
          isTopos : IsTopos A 1 ○ Ω ⊤ Ker char
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
+     Monik : {a : Obj A} (h : Hom A a Ω)  → Mono A (equalizer (Ker h))
+     Monik h = record { isMono = λ f g → monic (Ker h ) } 
 
 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( 1 : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
--- a/src/ToposEx.agda	Sat Feb 27 22:57:42 2021 +0900
+++ b/src/ToposEx.agda	Sun Feb 28 17:31:13 2021 +0900
@@ -101,6 +101,9 @@
             id1 A _ o g  ≈⟨ idL ⟩
             g ∎
 
+  open Equalizer
+  open import equalizer
+
   prop32→ :  {a b : Obj A}→ (f g : Hom A a b )
     → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ]
   prop32→ {a} {b} f g f=g = begin
@@ -108,10 +111,25 @@
             char t < id1 A b , id1 A b > δmono o < f , f >  ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
             char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f >    ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
             char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f)   ≈⟨ assoc ⟩
-            (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f   ≈⟨ {!!} ⟩
+            (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f ≈⟨ car lem1 ⟩
             (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
             ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
-            ⊤ t o  ○  a  ∎
+            ⊤ t o  ○  a  ∎ where
+               i = char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > 
+               e = Ker t ( ⊤ t o ○ b) 
+               ki =  IsEqualizer.k (isEqualizer e) (id1 A _) refl-hom
+               lem1 : (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) ≈ ( ⊤ t o  ○  b )
+               lem1 = begin
+                  i ≈↑⟨ idR ⟩
+                  i o id1 A _    ≈↑⟨ cdr (IsEqualizer.ek=h (isEqualizer e) ) ⟩
+                  i o (equalizer e o ki ) ≈⟨ assoc ⟩
+                  (i o equalizer e ) o ki ≈⟨ {!!} ⟩
+                  (((⊤ t) o (○ b)) o equalizer e ) o ki ≈⟨ car (IsEqualizer.fe=ge (isEqualizer e)) ⟩
+                  ((⊤ t o  ○  b) o equalizer e ) o  ki ≈↑⟨ assoc ⟩
+                  (⊤ t o  ○  b) o (equalizer e  o  ki )   ≈⟨ cdr (IsEqualizer.ek=h (isEqualizer e) )⟩
+                  (⊤ t o  ○  b) o id1 A _   ≈⟨ idR ⟩
+                  ⊤ t o  ○  b ∎ 
+               
 
   prop23→ :  {a b : Obj A}→ (f g : Hom A a b )
     → A [ A [ char t  < id1 A b , id1 A b > δmono  o < f , g > ]  ≈ A [ ⊤ t o  ○  a  ] ] → A [ f ≈ g ]