Mercurial > hg > Members > kono > Proof > category
changeset 984:949f83b3a8f0 Topos
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Mar 2021 16:26:00 +0900 |
| parents | 7ca3c84d4808 |
| children | 74728d51177b |
| files | src/ToposEx.agda |
| diffstat | 1 files changed, 25 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ToposEx.agda Wed Mar 03 16:11:01 2021 +0900 +++ b/src/ToposEx.agda Wed Mar 03 16:26:00 2021 +0900 @@ -119,6 +119,17 @@ id1 A _ o g ≈⟨ idL ⟩ g ∎ +-- +-- a -----------→ + +-- f||g ○ a | +-- ↓↓ | +-- b -----------→ 1 +-- | ○ b | +-- <1,1> | | ⊤ +-- ↓ ↓ +-- b ∧ b ---------→ Ω +-- char <1,1> + 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 @@ -154,6 +165,14 @@ open NatD open ToposNat n +-- 0 suc +-- 1 -----------→ N ---------→ N +-- | | | +-- | <f,g> | <f,g>| +-- | ↓ ↓ +-- 1 ---------→ N x A -----→ N x A +-- <0,z> <suc o π , h > + N : Obj A N = Nat TNat @@ -223,7 +242,12 @@ h o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ h o < id1 A N , g > ∎ - + -- . + -- / | \ + -- / | \ + -- / ↓ \ + -- N --→ N ←-- a + -- cor33 : coProduct A １ (Nat TNat ) -- N ≅ N + 1 cor33 = record { coproduct = N