Remove redundant clause for agda/agda#7496 (#1156)

agda · Sep 16, 2024 · e2370fb · e2370fb
1 parent 581748b
commit e2370fb
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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