/
PentagonId.agda
44 lines (34 loc) · 2.17 KB
/
PentagonId.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
open import Level
open import Function hiding ( id ) renaming ( _∘_ to _∘F_ )
open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open ≡-Reasoning
open import Theory.Triple renaming ( _,_,_ to _,'_,'_ )
open import Theory.Category.Definition
open import Theory.Category.Monoidal
open import Theory.Category.Isomorphism
open import Theory.Category.Examples using ( [_,_] ; setCategory ) renaming ( functorCategory to FunCat )
open import Theory.Functor.Definition
open import Theory.Functor.Composition
open import Theory.Functor.Association
open Theory.Functor.Association.Associator
open import Theory.Functor.Application
open Theory.Functor.Application.BiFunctor
open import Theory.Natural.Transformation
open import Theory.Natural.Transformation.Properties
open import Theory.Natural.Isomorphism
open import Theory.End.DayConvolution
open import Theory.End.DayUnit
open import Theory.Category.Monoidal.Examples.FunctorWithDayConvolution.Postulates
open import Extensionality
module Theory.Category.Monoidal.Examples.FunctorWithDayConvolution.Postulates.PentagonId where
open Category
open Functor hiding ( id )
open NaturalIsomorphism renaming ( η to iso-η )
postulate
day-pentagon-id : {ℓC₀ ℓC₁ : Level} → (ℓSet : Level) → {C : Category {ℓC₀} {ℓC₁}} → (CMon : MonoidalCategory C)
→ (w x y z : Functor C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁}))
→ ⟨ F₁ (dayConvolution {ℓSet = ℓSet} CMon) (id [ C , setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁} ] , iso-η (dayAssociator ℓSet CMon) (x ,' y ,' z)) ⟩∘ᵥ⟨
⟨ iso-η (dayAssociator ℓSet CMon) (w ,' F₀ (dayConvolution {ℓSet = ℓSet} CMon) (x , y) ,' z) ⟩∘ᵥ⟨
F₁ (dayConvolution {ℓSet = ℓSet} CMon) (iso-η (dayAssociator ℓSet CMon) (w ,' x ,' y) , id [ C , setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁} ]) ⟩ ⟩
≡ ⟨ iso-η (dayAssociator ℓSet CMon) (w ,' x ,' F₀ (dayConvolution {ℓSet = ℓSet} CMon) (y , z)) ⟩∘ᵥ⟨ iso-η (dayAssociator ℓSet CMon) (F₀ (dayConvolution {ℓSet = ℓSet} CMon) (w , x) ,' y ,' z) ⟩