Mercurial > hg > Members > kono > Proof > category
diff src/CCC.agda @ 1095:0211d99f29fc
Topos Sets char-iso done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 18 May 2021 15:38:46 +0900 |
| parents | 10b4d04b734f |
| children | 321f0fef54c2 |
line wrap: on
line diff
--- a/src/CCC.agda Tue May 18 01:06:43 2021 +0900 +++ b/src/CCC.agda Tue May 18 15:38:46 2021 +0900 @@ -251,11 +251,16 @@ 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-uniqueness : {a b : Obj A } {h : Hom A a Ω} → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ] + -- char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) → + -- Iso A a a' → A [ char p mp ≈ char q mq ] char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) → - Iso A a a' → A [ char p mp ≈ char q mq ] + (i : Iso A a a' ) → A [ p ≈ A [ q o Iso.≅→ i ] ] → A [ char p mp ≈ char q mq ] 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'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) + char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) ( begin + m ≈⟨ m=m' ⟩ + m' ≈↑⟨ idR ⟩ + m' o Iso.≅→ (≡-iso A b) ∎ ) 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-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 ] ]