diff options
| -rw-r--r-- | DecorationFunctor/Trivial.agda | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda index dee7c2e..3b88010 100644 --- a/DecorationFunctor/Trivial.agda +++ b/DecorationFunctor/Trivial.agda @@ -17,7 +17,7 @@ open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘_) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) -open import Categories.NaturalTransformation using (NaturalTransformation) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) @@ -47,9 +47,9 @@ F : Functor Nat (Setoids 0ℓ 0ℓ) F = record { F₀ = const (⊤-setoid) ; F₁ = const (record { to = const tt ; cong = const refl }) - ; identity = const refl - ; homomorphism = const refl - ; F-resp-≈ = const (const refl) + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = const refl } ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid @@ -59,10 +59,9 @@ F = record } ⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-) -⊗-homomorphism = record +⊗-homomorphism = ntHelper record { η = const (record { to = const tt ; cong = const refl }) - ; commute = const (const refl) - ; sym-commute = const (const refl) + ; commute = const refl } trivial : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) @@ -72,11 +71,11 @@ trivial = record { isMonoidal = record { ε = ε ; ⊗-homo = ⊗-homomorphism - ; associativity = const refl - ; unitaryˡ = const refl - ; unitaryʳ = const refl + ; associativity = refl + ; unitaryˡ = refl + ; unitaryʳ = refl } - ; braiding-compat = const refl + ; braiding-compat = refl } } |