Mercurial > hg > Members > kono > Proof > category
changeset 983:7ca3c84d4808
N ≅ N + 1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Mar 2021 16:11:01 +0900 |
| parents | 888e6613b99a |
| children | 949f83b3a8f0 |
| files | src/ToposEx.agda |
| diffstat | 1 files changed, 39 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ToposEx.agda Wed Mar 03 09:48:32 2021 +0900 +++ b/src/ToposEx.agda Wed Mar 03 16:11:01 2021 +0900 @@ -234,7 +234,7 @@ ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) ) ; κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g} ; uniqueness = uniq - ; +-cong = λ f=f' g=g' → {!!} -- prop33.g-cong p f=f' (resp refl-hom g=g' ) + ; +-cong = pcong } } where p : {a : Obj A} (f : Hom A １ a) ( h : Hom A (N ∧ a) a ) → prop33 f h @@ -252,13 +252,42 @@ uniq : {c : Obj A} {h : Hom A (Nat TNat) c} → prop33.g pp ≈ h uniq {c} {h} = begin - prop33.g pp ≈⟨⟩ - π' o gNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) {{!!}} {!!} {!!}) ⟩ - π' o {!!} ≈⟨ {!!} ⟩ + prop33.g pp ≈⟨⟩ + π' o gNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) ( + begin + < id1 A _ , h > o nzero TNat ≈⟨ IsCCC.distr-π isCCC ⟩ + < id1 A _ o nzero TNat , h o nzero TNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ + < nzero TNat , h o nzero TNat > ≈⟨⟩ + nzero (prop33.xnat pp) ∎ ) + (begin + < id1 A _ , h > o nsuc TNat ≈⟨ IsCCC.distr-π isCCC ⟩ + < id1 A _ o nsuc TNat , h o nsuc TNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ + < nsuc TNat , h o nsuc TNat > ≈↑⟨ IsCCC.π-cong isCCC idR idR ⟩ + < nsuc TNat o id1 A _ , (h o nsuc TNat ) o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) (cdr (IsCCC.e3a isCCC)) ⟩ + < nsuc TNat o ( π o < id1 A _ , h > ) , (h o nsuc TNat ) o ( π o < id1 A _ , h > ) > ≈⟨ IsCCC.π-cong isCCC assoc assoc ⟩ + < (nsuc TNat o π ) o < id1 A _ , h > , ((h o nsuc TNat ) o π ) o < id1 A _ , h > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ + < nsuc TNat o π , (h o nsuc TNat ) o π > o < id1 A _ , h > ≈⟨⟩ + nsuc (prop33.xnat pp) o < id1 A _ , h > ∎ )) ⟩ + π' o < id1 A _ , h > ≈⟨ IsCCC.e3b isCCC ⟩ h ∎ - - -- sym ( nat-unique ? (prop33.g0=f (p ( h o nzero TNat ) ( (h o nsuc TNat) o π) )) ? ) - - - - + pcong : {a : Obj A } {f f' : Hom A １ a } {g g' : Hom A (Nat TNat) a } → (f=f' : f ≈ f' ) → ( g=g' : g ≈ g' ) + → prop33.g (p f (g o π)) ≈ prop33.g (p f' (g' o π)) + pcong {a} {f} {f'} {g} {g'} f=f' g=g' = begin + prop33.g (p f (g o π)) ≈⟨⟩ + π' o (gNat (prop33.xnat (p f (g o π)))) ≈↑⟨ cdr (nat-unique (prop33.xnat (p f (g o π))) lem1 lem2 ) ⟩ + π' o (gNat (prop33.xnat (p f' (g' o π)))) ≈⟨⟩ + prop33.g (p f' (g' o π)) ∎ where + lem1 : A [ A [ gNat (prop33.xnat (p f' ((A Category.o g') π))) o nzero TNat ] ≈ nzero (prop33.xnat (p f ((A Category.o g) π))) ] + lem1 = begin + gNat (prop33.xnat (p f' (g' o π))) o nzero TNat ≈⟨ IsToposNat.izero isToposN _ ⟩ + nzero (prop33.xnat (p f' (g' o π))) ≈⟨⟩ + < nzero TNat , f' > ≈⟨ IsCCC.π-cong isCCC refl-hom (sym f=f') ⟩ + < nzero TNat , f > ≈⟨⟩ + nzero (prop33.xnat (p f (g o π))) ∎ + lem2 : A [ A [ gNat (prop33.xnat (p f' (g' o π))) o nsuc TNat ] ≈ A [ nsuc (prop33.xnat (p f (g o π))) o gNat (prop33.xnat (p f' (g' o π))) ] ] + lem2 = begin + gNat (prop33.xnat (p f' (g' o π))) o nsuc TNat ≈⟨ IsToposNat.isuc isToposN _ ⟩ + nsuc (prop33.xnat (p f' (g' o π))) o gNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ + < (nsuc TNat) o π , g' o π > o gNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ + < (nsuc TNat) o π , g o π > o gNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ + nsuc (prop33.xnat (p f (g o π))) o gNat (prop33.xnat (p f' (g' o π))) ∎