Mercurial > hg > Members > kono > Proof > category

changeset 978:db288effad97

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 20:49:13 +0900
parents 8ffdc897f29b
children 8e97363859ce
files src/ToposEx.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Tue Mar 02 17:56:31 2021 +0900
+++ b/src/ToposEx.agda	Tue Mar 02 20:49:13 2021 +0900
@@ -70,14 +70,14 @@
     ; π2 = ○ b   
     ; isPullback = record {
               commute = char-m=⊤ t m mono
-         ;    pullback = λ {d} {p1} {p2} eq →  
-             Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))  o IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq )
+         ;    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 = {!!}
       }
     } where
         f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))
+        f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))
         k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) →  A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono)))
         k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq )
         lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １)
@@ -87,6 +87,14 @@
            (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-char (isTopos t) m mono )) ⟩
            equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩
            p1 ∎
+        uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １)
+            (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 ∎
+
 
   δmono : {b : Obj A } → Mono A < id1 A b , id1 A b >
   δmono  = record {