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 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
private
α4⁻¹α-lhs α4⁻¹α-rhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') →
∀ x x' x'' x''' x'''' x'''''
→ (MonoidalCategory.C M) [ ? , ? ]
α4⁻¹α-lhs M x x' x'' x''' x'''' x''''' = {!!}
This gives me
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/MetaVars.hs:476:11 in Agd-2.7.0.1-cd9573e7:Agda.TypeChecking.MetaVars
but we should try to make an example that doesn't depend on the library. It goes away when you fill in some of the ?s so it's not stopping me from progress or anything
maxsnew
commented
1 month ago
This gives me
but we should try to make an example that doesn't depend on the library. It goes away when you fill in some of the
?s so it's not stopping me from progress or anything