Fix missed definition name change

agda · Oct 29, 2023 · cc9213f · cc9213f
1 parent dcd6d47
commit cc9213f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Data/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda
@@ -83,7 +83,7 @@ module _ where
             → A · (B + C) ≡ (A · B) + (A · C)
     ·LDist+ = ∥₂.elim3 (λ _ _ _ → isProp→isSet (isSetCard _ _))
                        λ _ _ _ → cong ∣_∣₂ (Σ≡Prop (λ _ → isPropIsSet)
-                                                   (isoToPath ×DistL⊎Iso))
+                                                   (isoToPath ×DistR⊎Iso))
 
     AnnihilL : (A : Card {ℓ}) → 𝟘 · A ≡ 𝟘
     AnnihilL = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _))