|
779
|
1 open import Level
|
|
|
2 open import Category
|
|
|
3 module CCC where
|
|
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
783
|
7 -- open import Data.Product renaming (_×_ to _∧_)
|
|
|
8 -- open import Category.Constructions.Product
|
|
780
|
9 open import Relation.Binary.PropositionalEquality
|
|
779
|
10
|
|
|
11 open Functor
|
|
|
12
|
|
|
13 -- ccc-1 : Hom A a 1 ≅ {*}
|
|
|
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
|
|
|
15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
|
|
|
16
|
|
|
17 data One {c : Level} : Set c where
|
|
|
18 OneObj : One -- () in Haskell ( or any one object set )
|
|
|
19
|
|
780
|
20 OneCat : Category Level.zero Level.zero Level.zero
|
|
|
21 OneCat = record {
|
|
|
22 Obj = One ;
|
|
|
23 Hom = λ a b → One ;
|
|
|
24 _o_ = λ{a} {b} {c} x y → OneObj ;
|
|
|
25 _≈_ = λ x y → x ≡ y ;
|
|
|
26 Id = λ{a} → OneObj ;
|
|
|
27 isCategory = record {
|
|
|
28 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ;
|
|
|
29 identityL = λ{a b f} → lemma {a} {b} {f} ;
|
|
|
30 identityR = λ{a b f} → lemma {a} {b} {f} ;
|
|
|
31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ;
|
|
|
32 associative = λ{a b c d f g h } → refl
|
|
|
33 }
|
|
|
34 } where
|
|
|
35 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f
|
|
|
36 lemma {a} {b} {f} with f
|
|
|
37 ... | OneObj = refl
|
|
|
38
|
|
783
|
39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B )
|
|
|
40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where
|
|
|
41 field
|
|
|
42 ≅→ : Hom A a b → Hom B a' b'
|
|
|
43 ≅← : Hom B a' b' → Hom A a b
|
|
|
44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ]
|
|
|
45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ]
|
|
779
|
46
|
|
783
|
47
|
|
|
48 record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _×_ : {a b c : Obj A ) → Hom A c a → Hom A c b → Hom A (a * b) )
|
|
780
|
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
779
|
50 field
|
|
783
|
51 ccc-1 : {a : Obj A} → -- Hom A a １ ≅ {*}
|
|
|
52 IsoS A OneCat a １ OneObj OneObj
|
|
780
|
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
|
|
783
|
54 IsoS A A c (a * b) {!!} {!!}
|
|
780
|
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
|
|
|
56 IsoS A A a (c ^ b) (a * b) c
|
|
779
|
57
|
|
|
58
|
|
781
|
59 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
60 field
|
|
|
61 one : Obj A
|
|
|
62 _*_ : Obj A → Obj A → Obj A
|
|
|
63 _^_ : Obj A → Obj A → Obj A
|
|
783
|
64 _×_ : Obj A → Obj A → Obj A
|
|
|
65 isCCC : IsCCC A one _×_ _*_ _^_
|
|
|
66
|
|
|
67 open import HomReasoning
|
|
|
68
|
|
|
69 record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
|
70 ( １ : Obj A )
|
|
|
71 ( ○ : (a : Obj A ) → Hom A a １ )
|
|
|
72 ( _∧_ : Obj A → Obj A → Obj A )
|
|
|
73 ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) )
|
|
|
74 ( π : {a b : Obj A } → Hom A (a ∧ b) a )
|
|
|
75 ( π' : {a b : Obj A } → Hom A (a ∧ b) b )
|
|
|
76 ( _<=_ : (a b : Obj A ) → Obj A )
|
|
|
77 ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) )
|
|
|
78 ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
|
|
|
79 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
80 field
|
|
|
81 -- cartesian
|
|
|
82 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
|
|
|
83 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ]
|
|
|
84 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ]
|
|
|
85 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ]
|
|
|
86 π-congl : {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ] → A [ < f , g > ≈ < f' , g > ]
|
|
|
87 π-congr : {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ] → A [ < f , g > ≈ < f , g' > ]
|
|
|
88 -- closed
|
|
|
89 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ]
|
|
|
90 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]
|
|
779
|
91
|
|
783
|
92 e'2 : A [ ○ １ ≈ id1 A １ ]
|
|
|
93 e'2 = let open ≈-Reasoning A in begin
|
|
|
94 ○ １
|
|
|
95 ≈↑⟨ e2 (id1 A １ ) ⟩
|
|
|
96 id1 A １
|
|
|
97 ∎
|
|
|
98 e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ]
|
|
|
99 e''2 {a} {b} {f} = let open ≈-Reasoning A in begin
|
|
|
100 ○ b o f
|
|
|
101 ≈⟨ e2 (○ b o f) ⟩
|
|
|
102 ○ a
|
|
|
103 ∎
|
|
|
104 distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ]
|
|
|
105 distr {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin
|
|
|
106 < f , g > o h
|
|
|
107 ≈↑⟨ e3c ⟩
|
|
|
108 < π o < f , g > o h , π' o < f , g > o h >
|
|
|
109 ≈⟨ π-congl assoc ⟩
|
|
|
110 < ( π o < f , g > ) o h , π' o < f , g > o h >
|
|
|
111 ≈⟨ π-congl (car e3a ) ⟩
|
|
|
112 < f o h , π' o < f , g > o h >
|
|
|
113 ≈⟨ π-congr assoc ⟩
|
|
|
114 < f o h , (π' o < f , g > ) o h >
|
|
|
115 ≈⟨ π-congr (car e3b ) ⟩
|
|
|
116 < f o h , g o h >
|
|
|
117 ∎
|
|
|
118 _×_ : { a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
|
|
|
119 f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] >
|
|
|
120
|
|
|
121 record EqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
781
|
122 field
|
|
783
|
123 １ : Obj A
|
|
|
124 ○ : (a : Obj A ) → Hom A a １
|
|
|
125 _∧_ : Obj A → Obj A → Obj A
|
|
|
126 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
|
|
|
127 π : {a b : Obj A } → Hom A (a ∧ b) a
|
|
|
128 π' : {a b : Obj A } → Hom A (a ∧ b) b
|
|
|
129 _<=_ : (a b : Obj A ) → Obj A
|
|
|
130 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
|
|
|
131 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
|
|
|
132 isEqCCC : IsEqCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε
|
|
781
|
133
|
|
783
|
134
|
|
|
135
|
|
|
136
|
|
|
137
|
