|
779
|
1 open import Level
|
|
|
2 open import Category
|
|
784
|
3 module CCChom where
|
|
779
|
4
|
|
|
5 open import HomReasoning
|
|
|
6 open import cat-utility
|
|
784
|
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
|
|
785
|
17 data One : Set where
|
|
779
|
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
|
|
785
|
35 lemma : {a b : One } → { f : One } → OneObj ≡ f
|
|
780
|
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 ]
|
|
787
|
46 cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ]
|
|
|
47 cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ]
|
|
779
|
48
|
|
783
|
49
|
|
784
|
50 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A)
|
|
780
|
51 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
779
|
52 field
|
|
785
|
53 ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a １ ≅ {*}
|
|
|
54 IsoS A OneCat a １ b c
|
|
780
|
55 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
|
|
784
|
56 IsoS A (A × A) c (a * b) (c , c ) (a , b )
|
|
780
|
57 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c
|
|
|
58 IsoS A A a (c ^ b) (a * b) c
|
|
788
|
59 nat-2 : {a b c : Obj A} → {f : Hom A (b * c) (b * c) } → {g : Hom A a (b * c) }
|
|
|
60 → (A × A) [ (A × A) [ IsoS.≅→ ccc-2 f o (g , g) ] ≈ IsoS.≅→ ccc-2 ( A [ f o g ] ) ]
|
|
789
|
61 nat-3 : {a b c : Obj A} → { k : Hom A c (a ^ b ) } → A [ A [ IsoS.≅→ (ccc-3) (id1 A (a ^ b)) o
|
|
|
62 (IsoS.≅← (ccc-2 ) (A [ k o (proj₁ ( IsoS.≅→ ccc-2 (id1 A (c * b)))) ] ,
|
|
|
63 (proj₂ ( IsoS.≅→ ccc-2 (id1 A (c * b) ))))) ] ≈ IsoS.≅→ (ccc-3 ) k ]
|
|
788
|
64
|
|
|
65 open import CCC
|
|
|
66
|
|
779
|
67
|
|
784
|
68 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
781
|
69 field
|
|
|
70 one : Obj A
|
|
|
71 _*_ : Obj A → Obj A → Obj A
|
|
|
72 _^_ : Obj A → Obj A → Obj A
|
|
784
|
73 isCCChom : IsCCChom A one _*_ _^_
|
|
783
|
74
|
|
|
75 open import HomReasoning
|
|
|
76
|
|
784
|
77 CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A
|
|
|
78 CCC→hom A c = record {
|
|
|
79 one = CCC.１ c
|
|
|
80 ; _*_ = CCC._∧_ c
|
|
|
81 ; _^_ = CCC._<=_ c
|
|
|
82 ; isCCChom = record {
|
|
787
|
83 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 }
|
|
|
84 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 }
|
|
|
85 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 }
|
|
789
|
86 ; nat-2 = nat-2 ; nat-3 = nat-3
|
|
784
|
87 }
|
|
785
|
88 } where
|
|
|
89 c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
|
|
|
90 c101 _ = OneObj
|
|
|
91 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c)
|
|
|
92 c102 {a} OneObj = CCC.○ c a
|
|
|
93 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f
|
|
|
94 c103 {a} {OneObj} {OneObj} {OneObj} = refl
|
|
|
95 c104 : {a : Obj A} → {f : Hom A a (CCC.１ c)} → A [ (c102 ( c101 f )) ≈ f ]
|
|
|
96 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f )
|
|
|
97 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
|
|
|
98 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] )
|
|
|
99 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
|
|
|
100 c202 (f , g ) = CCC.<_,_> c f g
|
|
|
101 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ]
|
|
|
102 c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c))
|
|
|
103 c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ]
|
|
|
104 c204 = IsCCC.e3c (CCC.isCCC c)
|
|
|
105 c301 : { d a b : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d -- a -> d <= b -> (a ∧ b ) -> d
|
|
|
106 c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ]
|
|
|
107 c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b)
|
|
|
108 c302 f = CCC._* c f
|
|
|
109 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ]
|
|
|
110 c303 = IsCCC.e4a (CCC.isCCC c)
|
|
|
111 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ]
|
|
|
112 c304 = IsCCC.e4b (CCC.isCCC c)
|
|
787
|
113 c105 : {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ]
|
|
|
114 c105 refl = let open ≈-Reasoning A in refl-hom
|
|
|
115 c106 : { a : Obj A } {f g : Hom A a (CCC.１ c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj} OneObj OneObj
|
|
|
116 c106 _ = refl
|
|
|
117 c205 : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ]
|
|
|
118 c205 f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g )
|
|
|
119 c206 : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ]
|
|
|
120 c206 {a} {b} {c₁} {f} {g} f=g = ( begin
|
|
|
121 CCC.π c o f
|
|
|
122 ≈⟨ cdr f=g ⟩
|
|
|
123 CCC.π c o g
|
|
|
124 ∎ ) , ( begin
|
|
|
125 CCC.π' c o f
|
|
|
126 ≈⟨ cdr f=g ⟩
|
|
|
127 CCC.π' c o g
|
|
|
128 ∎ ) where open ≈-Reasoning A
|
|
|
129 c305 : { a b c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ]
|
|
|
130 c305 f=g = IsCCC.*-cong (CCC.isCCC c ) f=g
|
|
|
131 c306 : { a b c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ]
|
|
|
132 c306 {a} {b} {c₁} {f} {g} f=g = begin
|
|
|
133 CCC.ε c o CCC.<_,_> c ( f o CCC.π c ) ( CCC.π' c )
|
|
|
134 ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g ) refl-hom) ⟩
|
|
|
135 CCC.ε c o CCC.<_,_> c ( g o CCC.π c ) ( CCC.π' c )
|
|
|
136 ∎ where open ≈-Reasoning A
|
|
788
|
137 nat-2 : {a b : Obj A} {c = c₁ : Obj A} {f : Hom A ((c CCC.∧ b) c₁) ((c CCC.∧ b) c₁)}
|
|
|
138 {g : Hom A a ((c CCC.∧ b) c₁)} → (A × A) [ (A × A) [ c201 f o g , g ] ≈ c201 (A [ f o g ]) ]
|
|
|
139 nat-2 {a} {b} {c₁} {f} {g} = ( begin
|
|
|
140 ( CCC.π c o f) o g
|
|
|
141 ≈↑⟨ assoc ⟩
|
|
|
142 ( CCC.π c ) o (f o g)
|
|
|
143 ∎ ) , (sym-hom assoc) where open ≈-Reasoning A
|
|
789
|
144 nat-3 : {a b : Obj A} {c = c₁ : Obj A} {k : Hom A c₁ ((c CCC.<= a) b)} →
|
|
|
145 A [ A [ c301 (id1 A ((c CCC.<= a) b)) o c202 (A [ k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) ] , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b)))) ]
|
|
|
146 ≈ c301 k ]
|
|
|
147 nat-3 {a} {b} { c₁} {k} = begin
|
|
|
148 c301 (id1 A ((c CCC.<= a) b)) o c202 ( k o proj₁ (c201 (id1 A ((c CCC.∧ c₁) b))) , proj₂ (c201 (id1 A ((c CCC.∧ c₁) b))))
|
|
|
149 ≈⟨⟩
|
|
|
150 ( CCC.ε c o CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
|
|
|
151 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b))))
|
|
|
152 ≈↑⟨ assoc ⟩
|
|
|
153 (CCC.ε c) o (( CCC.<_,_> c ((id1 A (CCC._<=_ c a b )) o CCC.π c) (CCC.π' c))
|
|
|
154 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
|
|
|
155 ≈⟨ cdr (car (IsCCC.π-cong (CCC.isCCC c ) idL refl-hom ) ) ⟩
|
|
|
156 (CCC.ε c) o ( CCC.<_,_> c (CCC.π c) (CCC.π' c)
|
|
|
157 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
|
|
|
158 ≈⟨ cdr (car (IsCCC.π-id (CCC.isCCC c))) ⟩
|
|
|
159 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b )
|
|
|
160 o (CCC.<_,_> c (k o ( CCC.π c o (id1 A (CCC._∧_ c c₁ b )))) ( CCC.π' c o (id1 A (CCC._∧_ c c₁ b)))))
|
|
|
161 ≈⟨ cdr ( cdr ( IsCCC.π-cong (CCC.isCCC c) (cdr idR) idR )) ⟩
|
|
|
162 (CCC.ε c) o ( id1 A (CCC._∧_ c ((c CCC.<= a) b) b ) o (CCC.<_,_> c (k o ( CCC.π c )) ( CCC.π' c )))
|
|
|
163 ≈⟨ cdr idL ⟩
|
|
|
164 (CCC.ε c) o (CCC.<_,_> c ( k o (CCC.π c) ) (CCC.π' c))
|
|
|
165 ≈⟨⟩
|
|
|
166 c301 k
|
|
|
167 ∎ where open ≈-Reasoning A
|
|
788
|
168
|
|
787
|
169
|
|
785
|
170
|
|
|
171 open CCChom
|
|
|
172 open IsCCChom
|
|
|
173 open IsoS
|
|
|
174
|
|
|
175 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
|
|
|
176 hom→CCC A h = record {
|
|
|
177 １ = １
|
|
|
178 ; ○ = ○
|
|
|
179 ; _∧_ = _/\_
|
|
|
180 ; <_,_> = <,>
|
|
|
181 ; π = π
|
|
|
182 ; π' = π'
|
|
|
183 ; _<=_ = _<=_
|
|
|
184 ; _* = _*
|
|
|
185 ; ε = ε
|
|
|
186 ; isCCC = isCCC
|
|
|
187 } where
|
|
|
188 １ : Obj A
|
|
|
189 １ = one h
|
|
|
190 ○ : (a : Obj A ) → Hom A a １
|
|
|
191 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
|
|
|
192 _/\_ : Obj A → Obj A → Obj A
|
|
|
193 _/\_ a b = _*_ h a b
|
|
|
194 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)
|
|
|
195 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
|
|
|
196 π : {a b : Obj A } → Hom A (a /\ b) a
|
|
|
197 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
|
|
|
198 π' : {a b : Obj A } → Hom A (a /\ b) b
|
|
|
199 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
|
|
|
200 _<=_ : (a b : Obj A ) → Obj A
|
|
|
201 _<=_ = _^_ h
|
|
|
202 _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b)
|
|
|
203 _* = ≅← ( ccc-3 (isCCChom h ) )
|
|
|
204 ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a
|
|
|
205 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b ))
|
|
|
206 isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε
|
|
|
207 isCCC = record {
|
|
|
208 e2 = e2
|
|
|
209 ; e3a = e3a
|
|
|
210 ; e3b = e3b
|
|
|
211 ; e3c = e3c
|
|
|
212 ; π-cong = π-cong
|
|
|
213 ; e4a = e4a
|
|
|
214 ; e4b = e4b
|
|
787
|
215 ; *-cong = *-cong
|
|
785
|
216 } where
|
|
786
|
217 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj
|
|
|
218 e20 OneObj = refl
|
|
785
|
219 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
|
|
786
|
220 e2 {a} f = begin
|
|
|
221 f
|
|
|
222 ≈↑⟨ iso← ( ccc-1 (isCCChom h )) ⟩
|
|
|
223 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj}) ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f )
|
|
|
224 ≈⟨ ≡-cong {Level.zero} {Level.zero} {Level.zero} {OneCat} {OneObj} {OneObj} (
|
|
|
225 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩
|
|
|
226 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj
|
|
|
227 ≈⟨⟩
|
|
|
228 ○ a
|
|
|
229 ∎ where open ≈-Reasoning A
|
|
787
|
230 --
|
|
|
231 -- g id
|
|
|
232 -- a -------------> b * c ------> b * c
|
|
|
233 --
|
|
|
234 -- a -------------> b * c ------> b
|
|
|
235 -- a -------------> b * c ------> c
|
|
|
236 --
|
|
|
237 cong-proj₁ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f ≈ proj₁ g ]
|
|
|
238 cong-proj₁ eq = proj₁ eq
|
|
788
|
239 cong-proj₂ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₂ f ≈ proj₂ g ]
|
|
|
240 cong-proj₂ eq = proj₂ eq
|
|
785
|
241 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
|
|
786
|
242 e3a {a} {b} {c} {f} {g} = begin
|
|
|
243 π o <,> f g
|
|
|
244 ≈⟨⟩
|
|
|
245 proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g))
|
|
788
|
246 ≈⟨ cong-proj₁ (nat-2 (isCCChom h)) ⟩
|
|
787
|
247 proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
|
|
|
248 ≈⟨ cong-proj₁ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
|
|
|
249 proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
|
|
|
250 ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩
|
|
786
|
251 proj₁ ( f , g )
|
|
|
252 ≈⟨⟩
|
|
|
253 f
|
|
|
254 ∎ where open ≈-Reasoning A
|
|
785
|
255 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
|
|
788
|
256 e3b {a} {b} {c} {f} {g} = begin
|
|
|
257 π' o <,> f g
|
|
|
258 ≈⟨⟩
|
|
|
259 proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g))
|
|
|
260 ≈⟨ cong-proj₂ (nat-2 (isCCChom h)) ⟩
|
|
|
261 proj₂ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
|
|
|
262 ≈⟨ cong-proj₂ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
|
|
|
263 proj₂ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
|
|
|
264 ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩
|
|
|
265 proj₂ ( f , g )
|
|
|
266 ≈⟨⟩
|
|
|
267 g
|
|
|
268 ∎ where open ≈-Reasoning A
|
|
785
|
269 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
|
|
788
|
270 e3c {a} {b} {c} {f} = begin
|
|
|
271 <,> ( π o f ) ( π' o f )
|
|
|
272 ≈⟨⟩
|
|
|
273 ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f
|
|
|
274 , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f )
|
|
|
275 ≈⟨⟩
|
|
|
276 ≅← (ccc-2 (isCCChom h)) (_[_o_] (A × A) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) (f , f ) )
|
|
|
277 ≈⟨ cong← (ccc-2 (isCCChom h)) (nat-2 (isCCChom h)) ⟩
|
|
|
278 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) o f ))
|
|
|
279 ≈⟨ cong← (ccc-2 (isCCChom h)) (cong→ (ccc-2 (isCCChom h)) idL ) ⟩
|
|
|
280 ≅← (ccc-2 (isCCChom h)) (≅→ (ccc-2 (isCCChom h)) f )
|
|
|
281 ≈⟨ iso← (ccc-2 (isCCChom h)) ⟩
|
|
|
282 f
|
|
|
283 ∎ where open ≈-Reasoning A
|
|
785
|
284 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ]
|
|
786
|
285 π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin
|
|
|
286 <,> f g
|
|
|
287 ≈⟨⟩
|
|
|
288 ≅← (ccc-2 (isCCChom h)) (f , g)
|
|
787
|
289 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩
|
|
786
|
290 ≅← (ccc-2 (isCCChom h)) (f' , g')
|
|
|
291 ≈⟨⟩
|
|
|
292 <,> f' g'
|
|
|
293 ∎ where open ≈-Reasoning A
|
|
|
294 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ]
|
|
|
295 e4a {a} {b} {c} {k} = begin
|
|
|
296 ε o ( <,> ((k *) o π ) π' )
|
|
|
297 ≈⟨⟩
|
|
787
|
298 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
|
|
789
|
299 ≈⟨ nat-3 (isCCChom h) ⟩
|
|
787
|
300 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k)
|
|
|
301 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩
|
|
786
|
302 k
|
|
|
303 ∎ where open ≈-Reasoning A
|
|
785
|
304 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
|
|
787
|
305 e4b {a} {b} {c} {k} = begin
|
|
|
306 ( ε o ( <,> ( k o π ) π' ) ) *
|
|
|
307 ≈⟨⟩
|
|
|
308 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π')))
|
|
789
|
309 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩
|
|
787
|
310 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
|
|
|
311 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩
|
|
|
312 k
|
|
|
313 ∎ where open ≈-Reasoning A
|
|
|
314 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
|
|
|
315 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
|
|
785
|
316
|
|
787
|
317
|
|
|
318
|
