From 537cd8123562290ffb08bfb787a56f7202a93e01 Mon Sep 17 00:00:00 2001 From: Szumi Xie Date: Sun, 15 Sep 2024 17:07:26 +0200 Subject: [PATCH] Remove redundant clause for agda/agda#7496 --- Cubical/HITs/SmashProduct/SymmetricMonoidal.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda index 1214b95c17..f1f3493260 100644 --- a/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda +++ b/Cubical/HITs/SmashProduct/SymmetricMonoidal.agda @@ -230,7 +230,6 @@ Bool⋀→ {A = A} (push (inr x) i) = pt A Bool⋀→ {A = A} (push (push a i₁) i) = pt A ⋀lIdIso : Iso (Bool*∙ {ℓ} ⋀ A) (typ A) -Iso.fun (⋀lIdIso {A = A}) (inl x) = pt A Iso.fun ⋀lIdIso = Bool⋀→ Iso.inv ⋀lIdIso a = inr (false* , a) Iso.rightInv ⋀lIdIso a = refl