Mercurial > hg > Members > kono > Proof > category
diff src/ToposEx.agda @ 973:5f76e5cf3d49
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Feb 2021 17:31:13 +0900 |
| parents | e05eb6029b5b |
| children | 5731ffd6cf7a |
line wrap: on
line diff
--- a/src/ToposEx.agda Sat Feb 27 22:57:42 2021 +0900 +++ b/src/ToposEx.agda Sun Feb 28 17:31:13 2021 +0900 @@ -101,6 +101,9 @@ id1 A _ o g ≈⟨ idL ⟩ g ∎ + open Equalizer + open import equalizer + 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 @@ -108,10 +111,25 @@ char t < id1 A b , id1 A b > δmono o < f , f > ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩ char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f > ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩ char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f) ≈⟨ assoc ⟩ - (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f ≈⟨ {!!} ⟩ + (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f ≈⟨ car lem1 ⟩ (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ - ⊤ t o ○ a ∎ + ⊤ t o ○ a ∎ where + i = char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > + e = Ker t ( ⊤ t o ○ b) + ki = IsEqualizer.k (isEqualizer e) (id1 A _) refl-hom + lem1 : (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) ≈ ( ⊤ t o ○ b ) + lem1 = begin + i ≈↑⟨ idR ⟩ + i o id1 A _ ≈↑⟨ cdr (IsEqualizer.ek=h (isEqualizer e) ) ⟩ + i o (equalizer e o ki ) ≈⟨ assoc ⟩ + (i o equalizer e ) o ki ≈⟨ {!!} ⟩ + (((⊤ t) o (○ b)) o equalizer e ) o ki ≈⟨ car (IsEqualizer.fe=ge (isEqualizer e)) ⟩ + ((⊤ t o ○ b) o equalizer e ) o ki ≈↑⟨ assoc ⟩ + (⊤ t o ○ b) o (equalizer e o ki ) ≈⟨ cdr (IsEqualizer.ek=h (isEqualizer e) )⟩ + (⊤ t o ○ b) o id1 A _ ≈⟨ idR ⟩ + ⊤ t o ○ b ∎ + 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 ]