Mercurial > hg > Members > kono > Proof > category
annotate src/bi-ccc.agda @ 968:3a096cb82dc4
Polynominal category and functional completeness begin
coMonad and coKleisli category
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Feb 2021 18:50:06 +0900 |
| parents | 472bcadfd216 |
| children | 45de2b31bf02 |
| rev | line source |
|---|---|
| 965 | 1 module bi-ccc where |
| 2 | |
| 3 open import Category | |
| 4 open import CCC | |
| 5 open import Level | |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 8 | |
| 9 record IsBICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
| 10 ( ⊥ : Obj A) -- ０ | |
| 11 ( □ : (a : Obj A ) → Hom A ⊥ a ) | |
| 12 ( _∨_ : Obj A → Obj A → Obj A ) | |
| 13 ( [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c ) | |
| 14 ( κ : {a b : Obj A } → Hom A a (a ∨ b) ) | |
| 15 ( κ' : {a b : Obj A } → Hom A b (a ∨ b) ) | |
| 16 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | |
| 17 field | |
| 18 e5 : {a : Obj A} → { f : Hom A ⊥ a } → A [ f ≈ □ a ] | |
| 19 e6a : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } → A [ A [ [ f , g ] o κ ] ≈ f ] | |
| 20 e6b : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } → A [ A [ [ f , g ] o κ' ] ≈ g ] | |
| 21 e6c : {a b c : Obj A} → { h : Hom A (a ∨ b ) c } → A [ [ A [ h o κ ] , A [ h o κ' ] ] ≈ h ] | |
| 22 κ-cong : {a b 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' ] ] | |
| 23 | |
| 24 record BICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | |
| 25 field | |
| 26 ⊥ : Obj A | |
| 27 □ : (a : Obj A ) → Hom A ⊥ a | |
| 28 _∨_ : Obj A → Obj A → Obj A | |
| 29 [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c | |
| 30 κ : {a b : Obj A } → Hom A a (a ∨ b) | |
| 31 κ' : {a b : Obj A } → Hom A b (a ∨ b) | |
| 32 isBICCC : IsBICCC A ⊥ □ _∨_ [_,_] κ κ' | |
| 33 | |
| 34 bi-ccc-⊥ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → (C : CCC A ) → (B : BICCC A ) → {a : Obj A} → Hom A a (BICCC.⊥ B) → Iso A a (BICCC.⊥ B) | |
| 35 bi-ccc-⊥ A C B {a} f = record { | |
| 36 ≅→ = f | |
| 37 ; ≅← = □ a | |
| 38 ; iso→ = bi-ccc-1 | |
| 39 ; iso← = bi-ccc-2 } where | |
| 40 open ≈-Reasoning A | |
| 41 open CCC.CCC C | |
| 42 open BICCC B | |
| 966 | 43 bi-hom← : {a c : Obj A } → Hom A (a ∧ ⊥) c → Hom A ⊥ (c <= a ) |
| 44 bi-hom← f = (f o < π' , π > ) * | |
| 45 bi-hom→ : {a c : Obj A } → Hom A ⊥ (c <= a ) → Hom A (a ∧ ⊥) c | |
| 46 bi-hom→ f = ε o ( < π' , π > o < π , f o π' > ) | |
| 47 bi-hom-iso : {a : Obj A } → {f : Hom A (a ∧ ⊥) (a ∧ ⊥)} → A [ bi-hom→ (bi-hom← f ) ≈ f ] | |
| 967 | 48 bi-hom-iso {a} {f} = begin |
| 49 bi-hom→ (bi-hom← f ) | |
| 50 ≈⟨⟩ | |
| 51 ε o ( < π' , π > o < π , ((f o < π' , π > ) *) o π' > ) | |
| 52 ≈⟨ cdr (IsCCC.π-exchg isCCC) ⟩ | |
| 53 ε o ( < ((f o < π' , π > ) *) o π' , π > ) | |
| 54 ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym idL)) ⟩ | |
| 55 ε o ( < ((f o < π' , π > ) *) o π' , id1 A _ o π > ) | |
| 56 ≈↑⟨ cdr (IsCCC.exchg-π isCCC) ⟩ | |
| 57 ε o (( < ((f o < π' , π > ) *) o π , id1 A _ o π' > ) o < π' , π > ) | |
| 58 ≈⟨ cdr (car ( IsCCC.π-cong isCCC refl-hom idL)) ⟩ | |
| 59 ε o (( < ((f o < π' , π > ) *) o π , π' > ) o < π' , π > ) | |
| 60 ≈⟨ assoc ⟩ | |
| 61 (ε o ( < ((f o < π' , π > ) *) o π , π' > )) o < π' , π > | |
| 62 ≈⟨ car (IsCCC.e4a isCCC) ⟩ | |
| 63 (f o < π' , π >) o < π' , π > | |
| 64 ≈⟨ sym assoc ⟩ | |
| 65 f o (< π' , π > o < π' , π >) | |
| 66 ≈⟨ cdr (IsCCC.π'π isCCC) ⟩ | |
| 67 f o id1 A _ | |
| 68 ≈⟨ idR ⟩ | |
| 69 f | |
| 70 ∎ | |
| 966 | 71 bi-hom-cong : {a c : Obj A } → {f g : Hom A ⊥ (c <= a )} → A [ f ≈ g ] → A [ bi-hom→ f ≈ bi-hom→ g ] |
| 967 | 72 bi-hom-cong f=g = cdr ( cdr (IsCCC.π-cong isCCC refl-hom (car f=g) )) |
| 965 | 73 bi-ccc-0 : A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ] |
| 74 bi-ccc-0 = begin | |
| 75 □ ( a ∧ ⊥ ) o π' | |
| 966 | 76 ≈↑⟨ bi-hom-iso ⟩ |
| 77 bi-hom→ (bi-hom← ( □ ( a ∧ ⊥ ) o π' )) | |
| 78 ≈⟨ bi-hom-cong (IsBICCC.e5 isBICCC ) ⟩ | |
| 79 bi-hom→ ( □ ( ( a ∧ ⊥ ) <= a) ) | |
| 80 ≈↑⟨ bi-hom-cong (IsBICCC.e5 isBICCC ) ⟩ | |
| 81 bi-hom→ (bi-hom← (id1 A ( a ∧ ⊥ ))) | |
| 82 ≈⟨ bi-hom-iso ⟩ | |
| 965 | 83 id1 A ( a ∧ ⊥ ) |
| 84 ∎ | |
| 85 bi-ccc-1 : A [ A [ □ a o f ] ≈ id1 A a ] | |
| 86 bi-ccc-1 = begin | |
| 87 □ a o f | |
| 88 ≈⟨ resp (sym (IsCCC.e3b isCCC) ) (sym ( IsBICCC.e5 isBICCC)) ⟩ | |
| 89 (π o □ ( a ∧ ⊥ )) o (π' o < id1 A a , f > ) | |
| 90 ≈⟨ sym assoc ⟩ | |
| 91 π o ( □ ( a ∧ ⊥ ) o (π' o < id1 A a , f > )) | |
| 92 ≈⟨ cdr (assoc) ⟩ | |
| 93 π o ( □ ( a ∧ ⊥ ) o π' ) o < id1 A a , f > | |
| 94 ≈⟨ cdr (car bi-ccc-0) ⟩ | |
| 95 π o id1 A _ o < id1 A a , f > | |
| 96 ≈⟨ cdr idL ⟩ | |
| 97 π o < id1 A a , f > | |
| 98 ≈⟨ IsCCC.e3a isCCC ⟩ | |
| 99 id1 A a | |
| 100 ∎ | |
| 101 bi-ccc-2 : A [ A [ f o □ a ] ≈ id1 A ⊥ ] | |
| 102 bi-ccc-2 = begin | |
| 103 f o □ a | |
| 104 ≈⟨ IsBICCC.e5 isBICCC ⟩ | |
| 105 □ _ | |
| 106 ≈↑⟨ IsBICCC.e5 isBICCC ⟩ | |
| 107 id1 A ⊥ | |
| 108 ∎ | |
| 109 | |
|
968
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
967
diff
changeset
|
110 -- define boolean category ( bi-cartesian closed category wth ⊤ and ⊥ object ) |
|
3a096cb82dc4
Polynominal category and functional completeness begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
967
diff
changeset
|
111 -- Any bi-cartesian closed category is isomorpphic to the boolean category |