Mercurial > hg > Members > kono > Proof > category

changeset 979:8e97363859ce

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 Wed, 03 Mar 2021 00:58:24 +0900
parents db288effad97
children 8ab4307d9337
files src/CCC.agda src/ToposEx.agda
diffstat 2 files changed, 41 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Tue Mar 02 20:49:13 2021 +0900
+++ b/src/CCC.agda	Wed Mar 03 00:58:24 2021 +0900
@@ -85,6 +85,20 @@
         ≈⟨ π-cong (cdr e3a)  (cdr e3b) ⟩
            < f o π' , g o π >
         ∎ 
+     π≈  : {a b c : Obj A} {f f' : Hom A c a }{g g' : Hom A c b }  → < f , g >  ≈  <  f' ,  g' >  → f  ≈ f'
+     π≈ {_} {_} {_} {f} {f'} {g} {g'}  eq = begin
+        f ≈↑⟨ e3a ⟩
+        π o < f , g >  ≈⟨ cdr eq ⟩
+        π o < f' , g' >  ≈⟨ e3a ⟩
+        f'
+        ∎ 
+     π'≈ : {a b c : Obj A} {f f' : Hom A c a }{g g' : Hom A c b }  → < f , g >  ≈  <  f' ,  g' >  → g  ≈ g'
+     π'≈ {_} {_} {_} {f} {f'} {g} {g'}  eq = begin
+        g ≈↑⟨ e3b ⟩
+        π' o < f , g >  ≈⟨ cdr eq ⟩
+        π' o < f' , g' >  ≈⟨ e3b ⟩
+        g'
+        ∎ 
      distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → ( h * o k )  ≈ ( h o < ( k o π ) , π' > )  * 
      distr-* {a} {b} {c} {d} {h} {k} = begin
              h * o k
--- a/src/ToposEx.agda	Tue Mar 02 20:49:13 2021 +0900
+++ b/src/ToposEx.agda	Wed Mar 03 00:58:24 2021 +0900
@@ -73,7 +73,7 @@
          ;    pullback = λ {d} {p1} {p2} eq →  f← o k  p1 p2 eq
          ;    π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq
          ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC))
-         ;    uniqueness = {!!}
+         ;    uniqueness = uniq
       }
     } where
         f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))
@@ -91,9 +91,17 @@
             (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) →
             A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → f← o k π1' π2' eq ≈ p' 
         uniq {d} p p1 p2 eq pe1 pe2 = begin
-             f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness  (isEqualizer (Ker t  (char t m mono))) {!!} ) ⟩
-             f← o (f→ o p ) ≈⟨ {!!} ⟩
-             p ∎
+             f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness  (isEqualizer (Ker t  (char t m mono))) lemma4) ⟩
+             f← o (f→ o p ) ≈⟨ assoc ⟩
+             (f← o f→ ) o p  ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))) ⟩
+             id1 A _ o p  ≈⟨ idL ⟩
+             p ∎ where
+                lemma4 : A [ A [ equalizer (Ker t (char t m mono)) o (f→ o p) ] ≈ p1 ]
+                lemma4 = begin
+                  equalizer (Ker t (char t m mono)) o (f→ o p)  ≈⟨ assoc ⟩
+                  (equalizer (Ker t (char t m mono)) o f→ ) o p  ≈⟨ car (IsoL.L≈iso (IsTopos.ker-char (isTopos t) m mono )) ⟩
+                  m o p  ≈⟨ pe1  ⟩
+                  p1 ∎ where
 
 
   δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
@@ -125,26 +133,23 @@
 
   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 ]
-  prop23→ {a} {b} f g eq = {!!} where
+  prop23→ {a} {b} f g eq = begin
+     f   ≈⟨ IsCCC.π≈ isCCC p2 ⟩
+     k   ≈↑⟨ IsCCC.π'≈ isCCC p2 ⟩
+     g   ∎
+     where
        δb : Hom A ( b ∧ b ) (Ω t)
        δb = char t  < id1 A b , id1 A b > δmono
        ip : Pullback A  δb  (⊤ t)
        ip = topos-m-pullback < id1 A b , id1 A b >  δmono
        k : Hom A a b
        k = IsPullback.pullback (Pullback.isPullback ip ) eq 
-       p0 : δb o ( Pullback.π1 ip o  k )  ≈  ⊤ t o ○ a 
-       p0 = begin
-            δb o ( Pullback.π1 ip o k ) ≈⟨⟩
-            char t < id1 A b , id1 A b > δmono o ( Pullback.π1 ip o k ) ≈⟨  {!!}  ⟩
-            char t < id1 A b , id1 A b > δmono o < f , g >  ≈⟨   eq ⟩
-            ⊤ t o ○ a  ∎
-       pf :  f ≈ id1 A b o k
-       pf =  {!!} -- IsPullback.uniqueness (Pullback.isPullback ip ) k  (Pullback.π1 ip o k )  (○  a) p0 refl-hom (IsCCC.e2 isCCC)
-       p2 :  < f , g > ≈ ( < id1 A b , id1 A b > o k )
+       p2 :  < f , g > ≈  < k , k >   
        p2 = begin
-            < f , g >   ≈⟨  IsCCC.π-cong isCCC  pf {!!} ⟩
-            < id1 A b o k  , id1 A b o k >   ≈↑⟨  IsCCC.distr-π isCCC  ⟩
-            < id1 A b , id1 A b > o k  ∎
+            < f , g >   ≈↑⟨ IsPullback.π1p=π1 (Pullback.isPullback ip) ⟩
+            < id1 A b , id1 A b > o k  ≈⟨ IsCCC.distr-π isCCC ⟩ 
+            < id1 A b o k , id1 A b o k >   ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ 
+            < k , k >  ∎
 
   N : (n : ToposNat A １ ) → Obj A
   N n = NatD.Nat (ToposNat.TNat n)
@@ -156,10 +161,12 @@
        gs=h : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nsuc  (ToposNat.TNat n) ]  ≈ A [ h o < id1 A _ , g f h > ] ]
        g-cong :  {a : Obj A} {f f' : Hom A １ a } { h h' : Hom A (N n ∧ a) a } →  A [ f ≈ f' ] → A [ h ≈ h' ] → A [ g f h ≈ g f' h' ]
 
+  p33 : (n : ToposNat A １ ) → prop33 n
+  p33 = {!!}
+
   cor33  : (n : ToposNat A １ )
-     → prop33 n 
      → coProduct A １ ( NatD.Nat (ToposNat.TNat n)  ) --  N ≅ N + 1
-  cor33 n p = record {
+  cor33 n = record {
         coproduct = N n
       ; κ1 = NatD.nzero (ToposNat.TNat n)
       ; κ2 = NatD.nsuc (ToposNat.TNat n)
@@ -172,6 +179,7 @@
 
        }
     } where
+        p = p33 n
         k2 : {a : Obj A} {f  : Hom A １ a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a }
            → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ]
         k2 {a} {f} {g} = begin