-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* some monoidal combinators, naturality proofs and an application of coherence * fix typo * one more that we need for Dyck Tracey
- Loading branch information
Showing
6 changed files
with
304 additions
and
75 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,79 @@ | ||
| {- Various large associator combinators etc -} | ||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Categories.Monoidal.Base | ||
| module Cubical.Categories.Monoidal.Combinators.Base | ||
| {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') where | ||
|
|
||
|
|
||
| import Cubical.Data.Equality as Eq | ||
| open import Cubical.Categories.Category | ||
| open import Cubical.Categories.Functor | ||
| open import Cubical.Categories.NaturalTransformation | ||
| open import Cubical.Categories.Constructions.BinProduct | ||
| open import Cubical.Categories.Constructions.BinProduct.More | ||
| open import Cubical.Categories.NaturalTransformation.More hiding (α) | ||
| open import Cubical.Categories.NaturalTransformation.Reind | ||
|
|
||
| private | ||
| module M = MonoidalCategory M | ||
| variable | ||
| v w x y z x' x'' x''' x'''' x''''' : M.ob | ||
|
|
||
| -- The 3 is the number of ⊗s involved, not objects. This would make α α2 | ||
| α2 = M.α | ||
|
|
||
| α3⟨_,_,_,_⟩ : ∀ w x y z → | ||
| M.Hom[ w M.⊗ (x M.⊗ (y M.⊗ z)) , (w M.⊗ (x M.⊗ y)) M.⊗ z ] | ||
| α3⟨ w , x , y , z ⟩ = M.α⟨ w , (x M.⊗ y) , z ⟩ M.∘ (M.id M.⊗ₕ M.α⟨ x , y , z ⟩) | ||
|
|
||
| α3⁻¹⟨_,_,_,_⟩ : ∀ w x y z → | ||
| M.Hom[ (w M.⊗ (x M.⊗ y)) M.⊗ z , w M.⊗ (x M.⊗ (y M.⊗ z)) ] | ||
| α3⁻¹⟨ w , x , y , z ⟩ = | ||
| (M.id M.⊗ₕ M.α⁻¹⟨ x , y , z ⟩) M.∘ M.α⁻¹⟨ w , x M.⊗ y , z ⟩ | ||
|
|
||
| α3 : NatIso {C = M.C ×C M.C ×C M.C ×C M.C}{D = M.C} | ||
| (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)))) | ||
| ((M.─⊗─ ∘F (M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C) ∘F | ||
| (𝟙⟨ M.C ⟩ ×F ((M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C))) | ||
| α3 = seqNatIso ((M.─⊗─ ∘ʳⁱ NatIso× (idNatIso 𝟙⟨ M.C ⟩) M.α)) | ||
| (reindNatIso _ _ _ _ (Eq.refl , Eq.refl) | ||
| ((M.α ∘ˡⁱ (𝟙⟨ M.C ⟩ ×F ((M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C))))) | ||
|
|
||
| private | ||
| testα3 : ∀ {w x y z} | ||
| → α3⟨ w , x , y , z ⟩ ≡ α3 .NatIso.trans ⟦ w , x , y , z ⟧ | ||
| testα3 = refl | ||
|
|
||
| testα⁻3 : ∀ {w x y z} | ||
| → α3⁻¹⟨ w , x , y , z ⟩ ≡ α3 .NatIso.nIso (w , x , y , z) .isIso.inv | ||
| testα⁻3 = refl | ||
|
|
||
| α4⟨_,_,_,_,_⟩ : ∀ v w x y z → | ||
| M.Hom[ v M.⊗ (w M.⊗ (x M.⊗ (y M.⊗ z))) , (v M.⊗ (w M.⊗ (x M.⊗ y))) M.⊗ z ] | ||
| α4⟨ v , w , x , y , z ⟩ = | ||
| M.α⟨ v , w M.⊗ (x M.⊗ y) , z ⟩ | ||
| M.∘ (M.id M.⊗ₕ α3⟨ w , x , y , z ⟩) | ||
|
|
||
| α4⁻¹⟨_,_,_,_,_⟩ : ∀ v w x y z → | ||
| M.Hom[ (v M.⊗ (w M.⊗ (x M.⊗ y))) M.⊗ z , v M.⊗ (w M.⊗ (x M.⊗ (y M.⊗ z))) ] | ||
| α4⁻¹⟨ v , w , x , y , z ⟩ = | ||
| M.id M.⊗ₕ α3⁻¹⟨ w , x , y , z ⟩ | ||
| M.∘ M.α⁻¹⟨ v , w M.⊗ (x M.⊗ y) , z ⟩ | ||
|
|
||
| α4 : NatIso {C = M.C ×C M.C ×C M.C ×C M.C ×C M.C}{D = M.C} | ||
| (M.─⊗─ | ||
| ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)))))) | ||
| ((M.─⊗─ ∘F (M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C) ∘F | ||
| (𝟙⟨ M.C ⟩ ×F | ||
| (((((M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)) ∘F ×C-assoc⁻ M.C M.C M.C) ×F | ||
| 𝟙⟨ M.C ⟩) | ||
| ∘F ×C-assoc (M.C ×C M.C) M.C M.C) | ||
| ∘F ×C-assoc M.C M.C (M.C ×C M.C)))) | ||
| α4 = seqNatIso | ||
| (((M.─⊗─ ∘ʳⁱ NatIso× (idNatIso 𝟙⟨ M.C ⟩) α3))) | ||
| (reindNatIso _ _ _ _ (Eq.refl , Eq.refl) | ||
| (M.α ∘ˡⁱ | ||
| (𝟙⟨ M.C ⟩ | ||
| ×F ((((M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)) ∘F ×C-assoc⁻ M.C M.C M.C ) ×F 𝟙⟨ M.C ⟩) | ||
| ∘F ×C-assoc (M.C ×C M.C) M.C M.C | ||
| ∘F ×C-assoc M.C M.C (M.C ×C M.C))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,102 @@ | ||
| {- Various large associator combinators etc -} | ||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Categories.Monoidal.Base | ||
| module Cubical.Categories.Monoidal.Combinators.Equations | ||
| where | ||
|
|
||
| open import Cubical.Foundations.HLevels | ||
| open import Cubical.Categories.Category | ||
| open import Cubical.Categories.Functor | ||
| open import Cubical.Categories.NaturalTransformation | ||
| open import Cubical.Categories.Constructions.BinProduct | ||
| open import Cubical.Categories.NaturalTransformation.More hiding (α) | ||
| open import Cubical.Categories.Monoidal.Functor | ||
| import Cubical.Categories.Monoidal.Combinators.Base as Combinators | ||
| open import Cubical.Categories.Constructions.Free.Monoidal.Base | ||
| open import Cubical.Categories.Constructions.Free.Monoidal.Coherence | ||
| open import Cubical.Data.SumFin | ||
|
|
||
| open Category | ||
| open Functor | ||
| private | ||
| α4⁻¹α-lhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') → | ||
| ∀ x x' x'' x''' x'''' x''''' | ||
| → (MonoidalCategory.C M) [ _ , _ ] | ||
| α4⁻¹α-lhs M x x' x'' x''' x'''' x''''' = | ||
| MComb.α4⁻¹⟨ x , x' , x'' , x''' , x'''' ⟩ M.⊗ₕ M.id {x'''''} | ||
| M.∘ M.α⟨ x M.⊗ (x' M.⊗ (x'' M.⊗ x''')) , x'''' , x''''' ⟩ | ||
| where module M = MonoidalCategory M | ||
| module MComb = Combinators M | ||
| α4⁻¹α-rhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') → | ||
| ∀ x x' x'' x''' x'''' x''''' | ||
| → (MonoidalCategory.C M) [ _ , _ ] | ||
| α4⁻¹α-rhs M x x' x'' x''' x'''' x''''' = | ||
| MComb.α4⟨ x , x' , x'' , x''' M.⊗ x'''' , x''''' ⟩ | ||
| M.∘ (M.id M.⊗ₕ (M.id M.⊗ₕ (M.id M.⊗ₕ M.α⟨ x''' , x'''' , x''''' ⟩))) | ||
| M.∘ MComb.α4⁻¹⟨ x , x' , x'' , x''' , x'''' M.⊗ x''''' ⟩ | ||
| where module M = MonoidalCategory M | ||
| module MComb = Combinators M | ||
|
|
||
| ηα-lhs ηα-rhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') → | ||
| ∀ x x' | ||
| → (MonoidalCategory.C M) [ _ , _ ] | ||
| ηα-lhs M x x' = (M.η⟨ x ⟩ M.⊗ₕ M.id {x'}) M.∘ M.α⟨ M.unit , x , x' ⟩ | ||
| where module M = MonoidalCategory M | ||
| ηα-rhs M x x' = M.η⟨ x M.⊗ x' ⟩ | ||
| where module M = MonoidalCategory M | ||
|
|
||
| private | ||
| F6 = FreeMonoidalCategory (Fin 6) | ||
| module F6 = MonoidalCategory F6 | ||
|
|
||
| x x' x'' x''' x'''' x''''' : F6.ob | ||
| x = ↑ (fromℕ 0) | ||
| x' = ↑ (fromℕ 1) | ||
| x'' = ↑ (fromℕ 2) | ||
| x''' = ↑ (fromℕ 3) | ||
| x'''' = ↑ (fromℕ 4) | ||
| x''''' = ↑ (fromℕ 5) | ||
| α4⁻¹α-free : | ||
| α4⁻¹α-lhs F6 x x' x'' x''' x'''' x''''' | ||
| ≡ α4⁻¹α-rhs F6 x x' x'' x''' x'''' x''''' | ||
| α4⁻¹α-free = coherence (Fin 6 , isSetFin) _ _ | ||
|
|
||
| α4⁻¹α : | ||
| ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') | ||
| → ∀ x x' x'' x''' x'''' x''''' | ||
| → α4⁻¹α-lhs M x x' x'' x''' x'''' x''''' | ||
| ≡ α4⁻¹α-rhs M x x' x'' x''' x'''' x''''' | ||
| α4⁻¹α M x x' x'' x''' x'''' x''''' = cong (sem.F .F-hom) α4⁻¹α-free | ||
| where | ||
| module M = MonoidalCategory M | ||
| ı : Fin 6 → M.ob | ||
| ı (inl _) = x | ||
| ı (fsuc (inl x₁)) = x' | ||
| ı (fsuc (fsuc (inl x₁))) = x'' | ||
| ı (fsuc (fsuc (fsuc (inl x₁)))) = x''' | ||
| ı (fsuc (fsuc (fsuc (fsuc (inl x₁))))) = x'''' | ||
| ı (fsuc (fsuc (fsuc (fsuc (fsuc (inl x₁)))))) = x''''' | ||
| sem = rec (Fin 6) M ı | ||
| module sem = StrongMonoidalFunctor sem | ||
|
|
||
| private | ||
| F2 = FreeMonoidalCategory (Fin 2) | ||
| module F2 = MonoidalCategory F2 | ||
|
|
||
| y y' : F2.ob | ||
| y = ↑ (fromℕ 0) | ||
| y' = ↑ (fromℕ 1) | ||
| ηα-free : ηα-lhs F2 y y' ≡ ηα-rhs F2 y y' | ||
| ηα-free = coherence (Fin 2 , isSetFin) _ _ | ||
|
|
||
| ηα : ∀ {ℓ ℓ'} (M : MonoidalCategory ℓ ℓ') | ||
| → ∀ x x' | ||
| → ηα-lhs M x x' ≡ ηα-rhs M x x' | ||
| ηα M x x' = cong (sem.F .F-hom) ηα-free | ||
| where | ||
| module M = MonoidalCategory M | ||
| ı : Fin 2 → M.ob | ||
| ı (inl x₁) = x | ||
| ı (fsuc x₁) = x' | ||
| sem = rec (Fin 2) M ı | ||
| module sem = StrongMonoidalFunctor sem |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.