Mercurial > hg > Members > kono > Proof > category

changeset 1071:167bb69baac9

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 Sat, 08 May 2021 12:37:01 +0900
parents ff1d4188f94d
children cf92383daef5
files src/CCC.agda
diffstat 1 files changed, 15 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Sat May 08 11:46:17 2021 +0900
+++ b/src/CCC.agda	Sat May 08 12:37:01 2021 +0900
@@ -230,19 +230,26 @@
         (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c 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-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
-             → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
+         ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
          char-iso  : {a b c : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
              → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ]
-         ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
-     char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
+         char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
              → A [ m  ≈  m'  ] → A [ char m mono ≈ char m' mono'  ]
-     char-cong  {a} {b} {m} {m'} {mono} {mono'}  m=m'  = begin
-            char m mono ≈⟨ {!!}   ⟩
-            char (equalizer (Ker {!!})) {!!}  ≈⟨ {!!}   ⟩
-            char m' mono' ∎  where   open ≈-Reasoning A
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
+     char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
+             → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
+     char-uniqueness {a} {b} {h}  = begin
+            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈⟨ char-cong {!!} ⟩
+            char ( ( equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ) (≡-mono h) ≈⟨ char-iso (≡-mono→ h) (≡-iso A _) ⟩
+            h ∎  where
+        open ≈-Reasoning A
+        ≡-mono : {a b : Obj A } (h : Hom A a Ω) →
+            Mono A ( ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))   o Iso.≅← (≡-iso A (equalizer-c (Ker h)))) 
+        ≡-mono = {!!}
+        ≡-mono→ : {a b : Obj A } (h : Hom A a Ω) →
+            Mono A ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))
+        ≡-mono→ = {!!}
      char-m=⊤ :  {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m) → A [ A [ char m mono  o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
      char-m=⊤ {a} {b} m mono  = begin
             char m mono  o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono)  ⟩