diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 10:59:04 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 10:59:04 -0600 |
| commit | 1a84efec2ba0769035144782e1e96a10e0d5a7b2 (patch) | |
| tree | 2be1a8bc1f809794b097320861c59b0b45cc689a /Functor/Monoidal/Strong/Properties.agda | |
| parent | f84a8d1bf9525aa9a005c1a31045b7685c6ac059 (diff) | |
Update to latest agda-categories
Diffstat (limited to 'Functor/Monoidal/Strong/Properties.agda')
| -rw-r--r-- | Functor/Monoidal/Strong/Properties.agda | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda index 9eb7579..a8b8279 100644 --- a/Functor/Monoidal/Strong/Properties.agda +++ b/Functor/Monoidal/Strong/Properties.agda @@ -75,9 +75,6 @@ module Shorthands where open Shorthands open HomReasoning -associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α -associativityᵢ = ⌞ associativity ⌟ - associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ associativity-inv = begin φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩ @@ -85,18 +82,12 @@ associativity-inv = begin (α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎ -unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ- -unitaryˡᵢ = ⌞ unitaryˡ ⌟ - unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐ unitaryˡ-inv = begin ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩ (ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩ λ⇐ ∎ -unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ -unitaryʳᵢ = ⌞ unitaryʳ ⌟ - unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐ unitaryʳ-inv = begin id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩ |