Skip to content

Commit 14fa916

Browse files
jacquescomeauxjacquescomeaux
committed
Continue cleaning up monoidal functor properties
1 parent 72ba594 commit 14fa916

File tree

1 file changed

+69
-60
lines changed

1 file changed

+69
-60
lines changed

‎src/Categories/Functor/Monoidal/Properties.agda‎

Lines changed: 69 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ open import Categories.Category.BinaryProducts using (BinaryProducts)
1111
open import Categories.Category.Core using (Category)
1212
open import Categories.Category.Monoidal.Bundle using (MonoidalCategory)
1313
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
14+
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
1415
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
1516
open import Categories.Category.Product using (_⁂_)
1617
open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘; [_]-resp-≅; [_]-resp-Iso)
@@ -21,7 +22,6 @@ open import Categories.NaturalTransformation using (NaturalTransformation; ntHel
2122
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
2223

2324
import Categories.Object.Terminal as ⊤
24-
import Categories.Object.Product as P
2525
import Categories.Morphism as M
2626
import Categories.Morphism.Reasoning as MR
2727
import Categories.Morphism.Properties as MP
@@ -57,6 +57,10 @@ private
5757
open Functor F public
5858
open IsStrongMonoidalFunctor F-IsStrongMonoidal public
5959
open MonoidalCategory D
60+
ε⇒ : unit ⇒ F₀ C.unit
61+
ε⇒ = ε.from
62+
ε⇐ : F₀ C.unit ⇒ unit
63+
ε⇐ = ε.to
6064
φ⇒ : {X Y : C.Obj} → F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y)
6165
φ⇒ {X} {Y} = ⊗-homo.⇒.η (X , Y)
6266
φ⇐ : {X Y : C.Obj} → F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y
@@ -112,7 +116,6 @@ module _ (A : MonoidalCategory o ℓ e) (B : MonoidalCategory o′ ℓ′ e′)
112116
module A = WithShorthands A
113117
module B = WithShorthands B
114118
module C = WithShorthands C
115-
open P C.U
116119
open M C.U
117120
open MR C.U
118121

@@ -187,7 +190,6 @@ module _ (A : MonoidalCategory o ℓ e) (B : MonoidalCategory o′ ℓ′ e′)
187190
module A = WithShorthands A
188191
module B = WithShorthands B
189192
module C = WithShorthands C
190-
open P C.U
191193
open M C.U
192194
open MR C.U
193195

@@ -228,85 +230,92 @@ module _ {A : MonoidalCategory o ℓ e} {B : MonoidalCategory o′ ℓ′ e′}
228230
where
229231
open MonoidalFunctor using (isMonoidal)
230232

233+
private
234+
235+
module WithCartesianShorthands (C : CartesianCategory o ℓ e) where
236+
open CartesianCategory C public
237+
open BinaryProducts products public renaming (_⁂_ to infixr 10 _×₁_)
238+
open CartesianMonoidal cartesian using (monoidal)
239+
open ⊗-Reasoning monoidal public
240+
open ⊤.Terminal terminal public
241+
231242
module _ (C : CartesianCategory o ℓ e) (D : CartesianCategory o′ ℓ′ e′) where
243+
232244
private
233-
module C = CartesianCategory C
234-
module D = CartesianCategory D
235-
module PC = BinaryProducts C.products
236-
module PD = BinaryProducts D.products
237-
module TC = ⊤.Terminal C.terminal
238-
module TD = ⊤.Terminal D.terminal
239-
open D.HomReasoning
240-
open MR D.U
245+
246+
module C = WithCartesianShorthands C
247+
module D = WithCartesianShorthands D
248+
open D hiding (project₁; project₂; unique)
249+
open MR U
241250

242251
module _ (F : StrongMonoidalFunctor C.monoidalCategory D.monoidalCategory) where
252+
243253
private
254+
244255
module F = StrongMonoidalFunctor F
256+
open FunctorShorthands.Strong F.isStrongMonoidal
245257

246-
F-resp-⊤ : ⊤.IsTerminal D.U (F.F₀ TC.⊤)
247-
F-resp-⊤ = ⊤.Terminal.⊤-is-terminal (⊤.transport-by-iso D.U D.terminal F.ε)
258+
F-resp-⊤ : ⊤.IsTerminal U (F₀ C.⊤)
259+
F-resp-⊤ = ⊤.Terminal.⊤-is-terminal (⊤.transport-by-iso D.U D.terminal ε)
248260
module F-resp-⊤ = ⊤.IsTerminal F-resp-⊤
249261

250-
lemma₁ : ∀ {X} → F.ε.from D.∘ TD.! {F.₀ X} D.≈ F.₁ (TC.! {X})
251-
lemma₁ = F-resp-⊤.!-unique _
262+
lemma₁ : ∀ {X} → F₁ (C.! {X}) ≈ ε⇒ ∘ !
263+
lemma₁ = Equiv.sym (F-resp-⊤.!-unique _)
252264

253-
π₁-comm : ∀ {X Y} → F.F₁ PC.π₁ D.∘ F.⊗-homo.⇒.η (X , Y) D.≈ PD.π₁
254-
π₁-comm {X} {Y} = begin
255-
F.F₁ PC.π₁ D.∘ F.⊗-homo.⇒.η (X , Y) ≈˘⟨ [ F.F ]-resp-∘ (C.Equiv.trans PC.project₁ C.identityˡ) ⟩∘⟨refl ⟩
256-
(F.F₁ PC.π₁ D.∘ F.F₁ (C.id PC.⁂ TC.!)) D.∘ F.⊗-homo.⇒.η (X , Y) ≈⟨ pullʳ (F.⊗-homo.⇒.sym-commute _) ⟩
257-
F.F₁ PC.π₁ D.∘ F.⊗-homo.⇒.η (X , TC.⊤) D.∘ (F.F₁ C.id PD.⁂ F.F₁ TC.!) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ([ F.₀ X PD.×- ]-resp-∘ lemma₁ ○ Functor.F-resp-≈ PD.-×- (⟺ F.identity , D.Equiv.refl)) ⟩
258-
F.F₁ PC.π₁ D.∘ F.⊗-homo.⇒.η (X , TC.⊤) D.∘ (D.id PD.⁂ F.ε.from) D.∘ (D.id PD.⁂ TD.!) ≈⟨ D.∘-resp-≈ʳ D.sym-assoc ○ D.sym-assoc ⟩
259-
(F.F₁ PC.π₁ D.∘ F.⊗-homo.⇒.η (X , TC.⊤) D.∘ (D.id PD.⁂ F.ε.from)) D.∘ (D.id PD.⁂ TD.!) ≈⟨ F.unitaryʳ ⟩∘⟨refl ⟩
260-
PD.π₁ D.∘ (D.id PD.⁂ TD.!) ≈⟨ PD.project₁ ○ D.identityˡ ⟩
261-
PD.π₁ ∎
265+
π₁-comm : ∀ {X Y} → F₁ C.π₁ ∘ φ⇒ {X} {Y} ≈ π₁
266+
π₁-comm = begin
267+
F₁ C.π₁ ∘ φ⇒ ≈⟨ pullˡ ([ F.F ]-resp-∘ (C.project₁ C.○ C.identityˡ)) ⟨
268+
F₁ C.π₁ ∘ F₁ (C.id C.×₁ C.!) ∘ φ⇒ ≈⟨ refl⟩∘⟨ ⊗-homo.⇒.sym-commute _ ⟩
269+
F₁ C.π₁ ∘ φ⇒ ∘ F₁ C.id ×₁ F₁ C.! ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identity ⟩⊗⟨ lemma₁ ⟩
270+
F₁ C.π₁ ∘ φ⇒ ∘ id ×₁ (ε⇒ ∘ !) ≈⟨ refl⟩∘⟨ pushʳ split₂ʳ ⟩
271+
F₁ C.π₁ ∘ (φ⇒ ∘ id ×₁ ε⇒) ∘ id ×₁ ! ≈⟨ pullˡ unitaryʳ ⟩
272+
π₁ ∘ id ×₁ ! ≈⟨ D.project₁ ○ identityˡ ⟩
273+
π₁ ∎
262274

263-
π₂-comm : ∀ {X Y} → F.F₁ PC.π₂ D.∘ F.⊗-homo.⇒.η (X , Y) D.≈ PD.π₂
275+
π₂-comm : ∀ {X Y} → F₁ C.π₂ ∘ φ⇒ {X} {Y} ≈ π₂
264276
π₂-comm {X} {Y} = begin
265-
F.F₁ PC.π₂ D.∘ F.⊗-homo.⇒.η (X , Y) ≈˘⟨ [ F.F ]-resp-∘ (C.Equiv.trans PC.project₂ C.identityˡ) ⟩∘⟨refl ⟩
266-
(F.F₁ PC.π₂ D.∘ F.F₁ (TC.! PC.⁂ C.id)) D.∘ F.⊗-homo.⇒.η (X , Y) ≈⟨ pullʳ (F.⊗-homo.⇒.sym-commute _) ⟩
267-
F.F₁ PC.π₂ D.∘ F.⊗-homo.⇒.η (TC.⊤ , Y) D.∘ (F.F₁ TC.! PD.⁂ F.F₁ C.id) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ([ PD.-× F.₀ Y ]-resp-∘ lemma₁ ○ Functor.F-resp-≈ PD.-×- (D.Equiv.refl , ⟺ F.identity)) ⟩
268-
F.F₁ PC.π₂ D.∘ F.⊗-homo.⇒.η (TC.⊤ , Y) D.∘ (F.ε.from PD.⁂ D.id) D.∘ (TD.! PD.⁂ D.id) ≈⟨ D.∘-resp-≈ʳ D.sym-assoc ○ D.sym-assoc ⟩
269-
(F.F₁ PC.π₂ D.∘ F.⊗-homo.⇒.η (TC.⊤ , Y) D.∘ (F.ε.from PD.⁂ D.id)) D.∘ (TD.! PD.⁂ D.id) ≈⟨ F.unitaryˡ ⟩∘⟨refl ⟩
270-
PD.π₂ D.∘ (TD.! PD.⁂ D.id) ≈⟨ PD.project₂ ○ D.identityˡ ⟩
271-
PD.π₂ ∎
272-
273-
unique : ∀ {X A B} {h : X D.⇒ F.₀ (A PC.× B)} {i : X D.⇒ F.₀ A} {j : X D.⇒ F.₀ B} →
274-
F.₁ PC.π₁ D.∘ h D.≈ i →
275-
F.₁ PC.π₂ D.∘ h D.≈ j →
276-
F.⊗-homo.⇒.η (A , B) D.∘ PD.⟨ i , j ⟩ D.≈ h
277-
unique eq₁ eq₂ = ⟺ (switch-tofromˡ F.⊗-homo.FX≅GX (⟺ (PD.unique (pullˡ (⟺ (switch-fromtoʳ F.⊗-homo.FX≅GX π₁-comm)) ○ eq₁)
278-
(pullˡ (⟺ (switch-fromtoʳ F.⊗-homo.FX≅GX π₂-comm)) ○ eq₂))))
277+
F₁ C.π₂ ∘ φ⇒ ≈⟨ pullˡ ([ F.F ]-resp-∘ (C.project₂ C.○ C.identityˡ)) ⟨
278+
F₁ C.π₂ ∘ F₁ (C.! C.×₁ C.id) ∘ φ⇒ ≈⟨ refl⟩∘⟨ ⊗-homo.⇒.sym-commute _ ⟩
279+
F₁ C.π₂ ∘ φ⇒ ∘ F₁ C.! ×₁ F₁ C.id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma₁ ⟩⊗⟨ identity ⟩
280+
F₁ C.π₂ ∘ φ⇒ ∘ (ε⇒ ∘ !) ×₁ id ≈⟨ refl⟩∘⟨ pushʳ split₁ʳ ⟩
281+
F₁ C.π₂ ∘ (φ⇒ ∘ ε⇒ ×₁ id) ∘ ! ×₁ id ≈⟨ pullˡ unitaryˡ ⟩
282+
π₂ ∘ ! ×₁ id ≈⟨ D.project₂ ○ identityˡ ⟩
283+
π₂ ∎
284+
285+
unique : ∀ {X A B} {h : X ⇒ F₀ (A C.× B)} {i : X ⇒ F₀ A} {j : X ⇒ F₀ B} →
286+
F₁ C.π₁ ∘ h ≈ i →
287+
F₁ C.π₂ ∘ h ≈ j →
288+
φ⇒ ∘ ⟨ i , j ⟩ ≈ h
289+
unique {h = h} {i} {j} eq₁ eq₂ = ⟺ (switch-tofromˡ ⊗-homo.FX≅GX (⟺ (D.unique eq₁′ eq₂′)))
290+
where
291+
eq₁′ : π₁ ∘ φ⇐ ∘ h ≈ i
292+
eq₁′ = pullˡ (⟺ (switch-fromtoʳ ⊗-homo.FX≅GX π₁-comm)) ○ eq₁
293+
eq₂′ : π₂ ∘ φ⇐ ∘ h ≈ j
294+
eq₂′ = pullˡ (⟺ (switch-fromtoʳ ⊗-homo.FX≅GX π₂-comm)) ○ eq₂
295+
296+
project₁ : {A B : C.Obj} {iA : D.Obj} {h : iA D.⇒ F₀ A} {i : iA ⇒ F₀ B} →
297+
F₁ C.π₁ ∘ φ⇒ ∘ ⟨ h , i ⟩ ≈ h
298+
project₁ {h = h} {i} = begin
299+
F.₁ C.π₁ ∘ φ⇒ ∘ ⟨ h , i ⟩ ≈⟨ pullˡ π₁-comm ⟩
300+
π₁ ∘ ⟨ h , i ⟩ ≈⟨ D.project₁ ⟩
301+
h ∎
302+
project₂ : {A B : C.Obj} {iA : Obj} {h : iA ⇒ F₀ A} {i : iA ⇒ F₀ B} →
303+
F₁ C.π₂ ∘ φ⇒ ∘ ⟨ h , i ⟩ ≈ i
304+
project₂ {h = h} {i} = begin
305+
F₁ C.π₂ ∘ φ⇒ ∘ ⟨ h , i ⟩ ≈⟨ pullˡ π₂-comm ⟩
306+
π₂ ∘ ⟨ h , i ⟩ ≈⟨ D.project₂ ⟩
307+
i ∎
279308

280309
StrongMonoidal⇒Cartesian : CartesianF C D
281310
StrongMonoidal⇒Cartesian = record
282311
{ F = F.F
283312
; isCartesian = record
284313
{ F-resp-⊤ = F-resp-⊤
285314
; F-resp-× = λ {A B} → record
286-
{ ⟨_,_⟩ = λ f g → F.⊗-homo.⇒.η _ D.∘ PD.⟨ f , g ⟩
315+
{ ⟨_,_⟩ = λ f g → φ⇒ ∘ ⟨ f , g ⟩
287316
; project₁ = project₁ {A} {B}
288317
; project₂ = project₂ {A} {B}
289318
; unique = unique
290319
}
291320
}
292321
}
293-
where
294-
import Categories.Object.Product.Core
295-
project₁ : {A B : C.Obj} {iA : D.Obj} {h : iA D.⇒ F.F₀ A} {i : iA D.⇒ F.F₀ B} →
296-
F.F₁ PC.π₁ D.∘
297-
F.⊗-homo.⇒.η (A , B) D.∘
298-
Categories.Object.Product.Core.Product.⟨ PD.product , h ⟩ i
299-
D.≈ h
300-
project₁ {A} {B} {_} {h} {i} = begin
301-
F.₁ PC.π₁ D.∘ F.⊗-homo.⇒.η _ D.∘ PD.⟨ h , i ⟩ ≈⟨ pullˡ π₁-comm ⟩
302-
PD.π₁ D.∘ PD.⟨ h , i ⟩ ≈⟨ PD.project₁ ⟩
303-
h ∎
304-
project₂ : {A B : C.Obj} {iA : D.Obj} {h : iA D.⇒ F.F₀ A} {i : iA D.⇒ F.F₀ B} →
305-
F.F₁ PC.π₂ D.∘
306-
F.⊗-homo.⇒.η (A , B) D.∘
307-
Categories.Object.Product.Core.Product.⟨ PD.product , h ⟩ i
308-
D.≈ i
309-
project₂ {_} {_} {_} {h} {i} = begin
310-
F.₁ PC.π₂ D.∘ F.⊗-homo.⇒.η _ D.∘ PD.⟨ h , i ⟩ ≈⟨ pullˡ π₂-comm ⟩
311-
PD.π₂ D.∘ PD.⟨ h , i ⟩ ≈⟨ PD.project₂ ⟩
312-
i ∎

0 commit comments

Comments
 (0)