|
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
|
|
|
43 bi-ccc-0 : A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
|
|
|
44 bi-ccc-0 = begin
|
|
|
45 □ ( a ∧ ⊥ ) o π'
|
|
|
46 ≈⟨ {!!} ⟩
|
|
|
47 id1 A ( a ∧ ⊥ )
|
|
|
48 ∎
|
|
|
49 bi-ccc-1 : A [ A [ □ a o f ] ≈ id1 A a ]
|
|
|
50 bi-ccc-1 = begin
|
|
|
51 □ a o f
|
|
|
52 ≈⟨ resp (sym (IsCCC.e3b isCCC) ) (sym ( IsBICCC.e5 isBICCC)) ⟩
|
|
|
53 (π o □ ( a ∧ ⊥ )) o (π' o < id1 A a , f > )
|
|
|
54 ≈⟨ sym assoc ⟩
|
|
|
55 π o ( □ ( a ∧ ⊥ ) o (π' o < id1 A a , f > ))
|
|
|
56 ≈⟨ cdr (assoc) ⟩
|
|
|
57 π o ( □ ( a ∧ ⊥ ) o π' ) o < id1 A a , f >
|
|
|
58 ≈⟨ cdr (car bi-ccc-0) ⟩
|
|
|
59 π o id1 A _ o < id1 A a , f >
|
|
|
60 ≈⟨ cdr idL ⟩
|
|
|
61 π o < id1 A a , f >
|
|
|
62 ≈⟨ IsCCC.e3a isCCC ⟩
|
|
|
63 id1 A a
|
|
|
64 ∎
|
|
|
65 bi-ccc-2 : A [ A [ f o □ a ] ≈ id1 A ⊥ ]
|
|
|
66 bi-ccc-2 = begin
|
|
|
67 f o □ a
|
|
|
68 ≈⟨ IsBICCC.e5 isBICCC ⟩
|
|
|
69 □ _
|
|
|
70 ≈↑⟨ IsBICCC.e5 isBICCC ⟩
|
|
|
71 id1 A ⊥
|
|
|
72 ∎
|
|
|
73
|
