Mercurial > hg > Members > kono > Proof > category
changeset 972:e05eb6029b5b
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 27 Feb 2021 22:57:42 +0900 |
parents | 9746e93a8c31 |
children | 5f76e5cf3d49 |
files | src/ToposEx.agda src/cat-utility.agda |
diffstat | 2 files changed, 43 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ToposEx.agda Sat Feb 27 12:15:28 2021 +0900 +++ b/src/ToposEx.agda Sat Feb 27 22:57:42 2021 +0900 @@ -91,11 +91,27 @@ isMono = m1 } where m1 : {d b : Obj A} (f g : Hom A d b) → A [ A [ < id1 A b , id1 A b > o f ] ≈ A [ < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ] - m1 {d} {b} f g = {!!} + m1 {d} {b} f g eq = begin + f ≈↑⟨ idL ⟩ + id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩ + (π o < id1 A b , id1 A b >) o f ≈↑⟨ assoc ⟩ + π o (< id1 A b , id1 A b > o f) ≈⟨ cdr eq ⟩ + π o (< id1 A b , id1 A b > o g) ≈⟨ assoc ⟩ + (π o < id1 A b , id1 A b >) o g ≈⟨ car (IsCCC.e3a isCCC) ⟩ + id1 A _ o g ≈⟨ idL ⟩ + g ∎ 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→ = {!!} + prop32→ {a} {b} f g f=g = begin + char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g)) ⟩ + 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 ≈⟨ {!!} ⟩ + (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ + ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ + ⊤ t o ○ a ∎ 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 ] @@ -104,25 +120,37 @@ N : (n : ToposNat A 1 ) → Obj A N n = NatD.Nat (ToposNat.TNat n) - record prop33 (n : ToposNat A 1 ) {a : Obj A} (f : Hom A 1 a ) ( h : Hom A (N n ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where + record prop33 (n : ToposNat A 1 ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - g : Hom A (N n) a - g0=f : A [ A [ g o NatD.nzero (ToposNat.TNat n) ] ≈ f ] - gs=h : A [ A [ g o NatD.nsuc (ToposNat.TNat n) ] ≈ A [ h o < id1 A _ , g > ] ] + g : {a : Obj A} (f : Hom A 1 a ) ( h : Hom A (N n ∧ a) a ) → Hom A (N n) a + g0=f : {a : Obj A} (f : Hom A 1 a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nzero (ToposNat.TNat n) ] ≈ f ] + gs=h : {a : Obj A} (f : Hom A 1 a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nsuc (ToposNat.TNat n) ] ≈ A [ h o < id1 A _ , g f h > ] ] + g-cong : {a : Obj A} {f f' : Hom A 1 a } { h h' : Hom A (N n ∧ a) a } → A [ f ≈ f' ] → A [ h ≈ h' ] → A [ g f h ≈ g f' h' ] cor33 : (n : ToposNat A 1 ) - → ( {a : Obj A} (f : Hom A 1 a ) ( h : Hom A (N n ∧ a) a ) → prop33 n f h ) + → prop33 n → coProduct A 1 ( NatD.Nat (ToposNat.TNat n) ) -- N ≅ N + 1 cor33 n p = record { coproduct = N n ; κ1 = NatD.nzero (ToposNat.TNat n) - ; κ2 = id1 A (N n) + ; κ2 = NatD.nsuc (ToposNat.TNat n) ; isProduct = record { - _+_ = λ {a} f g → prop33.g ( p {a} f π' ) - ; κ1fxg=f = λ {a} {f} {g} → prop33.g0=f (p f π' ) - ; κ2fxg=g = λ {a} {f} {g} → ? + _+_ = λ {a} f g → prop33.g p f ( g o π ) -- Hom A (N n ∧ a) a + ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f p f (g o π ) + ; κ2f+g=g = k2 ; uniqueness = {!!} - ; +-cong = {!!} + ; +-cong = λ f=f' g=g' → prop33.g-cong p f=f' (resp refl-hom g=g' ) } - } + } where + k2 : {a : Obj A} {f : Hom A 1 a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a } + → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ] + k2 {a} {f} {g} = begin + (prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n)) ≈⟨ prop33.gs=h p f (g o π ) ⟩ + ( g o π ) o < id1 A (N n) , prop33.g p f (g o π) > ≈⟨ sym assoc ⟩ + g o ( π o < id1 A (N n) , prop33.g p f (g o π) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ + g o id1 A (N n) ≈⟨ idR ⟩ + g ∎ + + +
--- a/src/cat-utility.agda Sat Feb 27 12:15:28 2021 +0900 +++ b/src/cat-utility.agda Sat Feb 27 22:57:42 2021 +0900 @@ -253,8 +253,8 @@ : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field _+_ : {c : Obj A} ( f : Hom A a c ) → ( g : Hom A b c ) → Hom A ab c - κ1fxg=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1 ] ≈ f ] - κ2fxg=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2 ] ≈ g ] + κ1f+g=f : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ1 ] ≈ f ] + κ2f+g=g : {c : Obj A} { f : Hom A a c } → { g : Hom A b c } → A [ A [ ( f + g ) o κ2 ] ≈ g ] uniqueness : {c : Obj A} { h : Hom A ab c } → A [ ( A [ h o κ1 ] ) + ( A [ h o κ2 ] ) ≈ h ] +-cong : {c : Obj A} { f f' : Hom A a c } → { g g' : Hom A b c } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f + g ≈ f' + g' ]