annotate src/bi-ccc.agda @ 985:74728d51177b

Added tag Topos for changeset 949f83b3a8f0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Mar 2021 16:30:40 +0900
parents 3a096cb82dc4
children 45de2b31bf02
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
965
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module bi-ccc where
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import CCC
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Level
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import HomReasoning
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import cat-utility
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 record IsBICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 ( ⊥ : Obj A) -- 0
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 ( □ : (a : Obj A ) → Hom A ⊥ a )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ( _∨_ : Obj A → Obj A → Obj A )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ( [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ( κ : {a b : Obj A } → Hom A a (a ∨ b) )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 ( κ' : {a b : Obj A } → Hom A b (a ∨ b) )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 e5 : {a : Obj A} → { f : Hom A ⊥ a } → A [ f ≈ □ a ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 e6a : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } → A [ A [ [ f , g ] o κ ] ≈ f ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 e6b : {a b c : Obj A} → { f : Hom A a c }{ g : Hom A b c } → A [ A [ [ f , g ] o κ' ] ≈ g ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 e6c : {a b c : Obj A} → { h : Hom A (a ∨ b ) c } → A [ [ A [ h o κ ] , A [ h o κ' ] ] ≈ h ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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' ] ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 record BICCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 field
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 ⊥ : Obj A
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 □ : (a : Obj A ) → Hom A ⊥ a
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _∨_ : Obj A → Obj A → Obj A
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 [_,_] : {a b c : Obj A } → Hom A a c → Hom A b c → Hom A (a ∨ b) c
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 κ : {a b : Obj A } → Hom A a (a ∨ b)
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 κ' : {a b : Obj A } → Hom A b (a ∨ b)
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 isBICCC : IsBICCC A ⊥ □ _∨_ [_,_] κ κ'
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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)
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 bi-ccc-⊥ A C B {a} f = record {
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 ≅→ = f
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ; ≅← = □ a
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ; iso→ = bi-ccc-1
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; iso← = bi-ccc-2 } where
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 open ≈-Reasoning A
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 open CCC.CCC C
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 open BICCC B
966
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
43 bi-hom← : {a c : Obj A } → Hom A (a ∧ ⊥) c → Hom A ⊥ (c <= a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
44 bi-hom← f = (f o < π' , π > ) *
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
45 bi-hom→ : {a c : Obj A } → Hom A ⊥ (c <= a ) → Hom A (a ∧ ⊥) c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
46 bi-hom→ f = ε o ( < π' , π > o < π , f o π' > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
47 bi-hom-iso : {a : Obj A } → {f : Hom A (a ∧ ⊥) (a ∧ ⊥)} → A [ bi-hom→ (bi-hom← f ) ≈ f ]
967
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
48 bi-hom-iso {a} {f} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
49 bi-hom→ (bi-hom← f )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
50 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
51 ε o ( < π' , π > o < π , ((f o < π' , π > ) *) o π' > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
52 ≈⟨ cdr (IsCCC.π-exchg isCCC) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
53 ε o ( < ((f o < π' , π > ) *) o π' , π > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
54 ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym idL)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
55 ε o ( < ((f o < π' , π > ) *) o π' , id1 A _ o π > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
56 ≈↑⟨ cdr (IsCCC.exchg-π isCCC) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
57 ε o (( < ((f o < π' , π > ) *) o π , id1 A _ o π' > ) o < π' , π > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
58 ≈⟨ cdr (car ( IsCCC.π-cong isCCC refl-hom idL)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
59 ε o (( < ((f o < π' , π > ) *) o π , π' > ) o < π' , π > )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
60 ≈⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
61 (ε o ( < ((f o < π' , π > ) *) o π , π' > )) o < π' , π >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
62 ≈⟨ car (IsCCC.e4a isCCC) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
63 (f o < π' , π >) o < π' , π >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
64 ≈⟨ sym assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
65 f o (< π' , π > o < π' , π >)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
66 ≈⟨ cdr (IsCCC.π'π isCCC) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
67 f o id1 A _
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
68 ≈⟨ idR ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
69 f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
70
966
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 966
diff changeset
72 bi-hom-cong f=g = cdr ( cdr (IsCCC.π-cong isCCC refl-hom (car f=g) ))
965
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 bi-ccc-0 : A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 bi-ccc-0 = begin
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 □ ( a ∧ ⊥ ) o π'
966
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
76 ≈↑⟨ bi-hom-iso ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
77 bi-hom→ (bi-hom← ( □ ( a ∧ ⊥ ) o π' ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
78 ≈⟨ bi-hom-cong (IsBICCC.e5 isBICCC ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
79 bi-hom→ ( □ ( ( a ∧ ⊥ ) <= a) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
80 ≈↑⟨ bi-hom-cong (IsBICCC.e5 isBICCC ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
81 bi-hom→ (bi-hom← (id1 A ( a ∧ ⊥ )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 965
diff changeset
82 ≈⟨ bi-hom-iso ⟩
965
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 id1 A ( a ∧ ⊥ )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 bi-ccc-1 : A [ A [ □ a o f ] ≈ id1 A a ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 bi-ccc-1 = begin
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 □ a o f
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 ≈⟨ resp (sym (IsCCC.e3b isCCC) ) (sym ( IsBICCC.e5 isBICCC)) ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 (π o □ ( a ∧ ⊥ )) o (π' o < id1 A a , f > )
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 ≈⟨ sym assoc ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 π o ( □ ( a ∧ ⊥ ) o (π' o < id1 A a , f > ))
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 ≈⟨ cdr (assoc) ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 π o ( □ ( a ∧ ⊥ ) o π' ) o < id1 A a , f >
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 ≈⟨ cdr (car bi-ccc-0) ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 π o id1 A _ o < id1 A a , f >
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 ≈⟨ cdr idL ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 π o < id1 A a , f >
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 ≈⟨ IsCCC.e3a isCCC ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 id1 A a
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 bi-ccc-2 : A [ A [ f o □ a ] ≈ id1 A ⊥ ]
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 bi-ccc-2 = begin
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 f o □ a
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ≈⟨ IsBICCC.e5 isBICCC ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 □ _
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ≈↑⟨ IsBICCC.e5 isBICCC ⟩
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 id1 A ⊥
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
396bf884f5e7 bi-cartesian
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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