Mercurial > hg > Members > kono > Proof > category

changeset 976:73fd14a73d49

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, 02 Mar 2021 09:48:12 +0900
parents f8fba4f1dcfa
children 8ffdc897f29b
files src/ToposEx.agda src/cat-utility.agda src/pullback.agda
diffstat 3 files changed, 39 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Mon Mar 01 17:01:00 2021 +0900
+++ b/src/ToposEx.agda	Tue Mar 02 09:48:12 2021 +0900
@@ -55,15 +55,26 @@
              ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq)          ≈⟨ e2 ⟩
              ○ d ≈↑⟨ e2 ⟩
              p2' ∎ 
-    uniq :  {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) {π1' : Hom A d a} {π2' : Hom A d １} {eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]}
-            {π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]} {π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]}
+    uniq :  {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) (π1' : Hom A d a) (π2' : Hom A d １) (eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ])
+            (π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]) (π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ])
              → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (lemma1 π1' π2' eq) ≈ p' ]
-    uniq {d} (p') {p1'} {p2'} {eq} {pe1} {pe2} = begin
+    uniq {d} (p') p1' p2' eq pe1 pe2 = begin
              IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq)  ≈⟨ IsEqualizer.uniqueness  (isEqualizer (Ker t h)) pe1 ⟩
              p' ∎ 
 
   topos-m-pullback : {a b : Obj A}  → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono )  (⊤ t)
-  topos-m-pullback {a} {b} m mono  = topos-pullback {a} (char t m mono)
+  topos-m-pullback {a} {b} m mono  = record {
+      ab = b     
+    ; π1 = m    
+    ; π2 = ○ b   
+    ; isPullback = record {
+              commute = char-m=⊤ t m mono
+         ;    pullback = λ {d} {p1} {p2} eq → {!!} -- Iso.≅← (IsTopos.ker-char (isTopos t) ? ? )  -- IsEqualizer.k (isEqualizer (Ker t ?)) ? ?
+         ;    π1p=π1 = {!!} -- IsEqualizer.ek=h (isEqualizer (Ker t h))
+         ;    π2p=π2 = {!!} -- λ {d} {p1'} {p2'} {eq} → lemma2 eq
+         ;    uniqueness = {!!}
+      }
+    } where
 
   δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
   δmono  = record {
@@ -80,9 +91,6 @@
             id1 A _ o g  ≈⟨ idL ⟩
             g ∎
 
-  ip : {b : Obj A } → Pullback A  (char t  < id1 A b , id1 A b > δmono )  (⊤ t)
-  ip {b} = topos-m-pullback  < id1 A b , id1 A b > δmono
-
   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
@@ -97,7 +105,22 @@
 
   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→ = {!!}
+  prop23→ {a} {b} f g eq = {!!} 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 
+       -- δb o (A Category.o Pullback.π1 ip) k  ≈  ⊤ t o ○ a 
+       -- Pullback.π1 ip o k  ≈ < f , g >
+       pf :  f ≈ id1 A b o k
+       pf =  IsPullback.uniqueness (Pullback.isPullback ip ) k < f , g >  (○  a) eq {!!} (IsCCC.e2 isCCC)
+       p2 :  < f , g > ≈ ( < id1 A b , id1 A b > o 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  ∎
 
   N : (n : ToposNat A １ ) → Obj A
   N n = NatD.Nat (ToposNat.TNat n)
--- a/src/cat-utility.agda	Mon Mar 01 17:01:00 2021 +0900
+++ b/src/cat-utility.agda	Tue Mar 02 09:48:12 2021 +0900
@@ -328,9 +328,9 @@
                      →  A [ A [ π1  o pullback eq ] ≈  π1' ]
               π2p=π2 :  { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f  o π1' ] ≈ A [ g  o π2' ]  ] }
                      →  A [ A [ π2  o pullback eq ] ≈  π2' ]
-              uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f  o π1' ] ≈ A [ g  o π2' ] ]  }
-                     →  { π1p=π1' : A [ A [ π1  o p' ] ≈  π1' ] }
-                     →  { π2p=π2' : A [ A [ π2  o p' ] ≈  π2' ] }
+              uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → ( π1' : Hom A d a ) ( π2' : Hom A d b ) → ( eq : A [ A [ f  o π1' ] ≈ A [ g  o π2' ] ]  )
+                     →  ( π1p=π1' : A [ A [ π1  o p' ] ≈  π1' ] )
+                     →  ( π2p=π2' : A [ A [ π2  o p' ] ≈  π2' ] )
                      →  A [ pullback eq  ≈ p' ]
 
         record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {a b c : Obj A}
--- a/src/pullback.agda	Mon Mar 01 17:01:00 2021 +0900
+++ b/src/pullback.agda	Tue Mar 02 09:48:12 2021 +0900
@@ -116,12 +116,12 @@
              ≈⟨ π2fxg=g prod ⟩
                      π2'
              ∎
-      uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} 
-         {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
-        {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
-        {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
+      uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) (π1' : Hom A d₁ a) (π2' : Hom A d₁ b)
+         (eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]) →
+        (eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]) →
+        (eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]) →
         A [ p1 eq ≈ p' ]
-      uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
+      uniqueness1 {d'} p' π1' π2' eq eq1 eq2 = let open ≈-Reasoning (A) in
              begin
                  p1 eq
              ≈⟨⟩