From cc9213fdfe9b0b662124e45b2662658e1d3cfd1b Mon Sep 17 00:00:00 2001 From: LuuBluum Date: Sun, 29 Oct 2023 06:56:52 +0000 Subject: [PATCH] Fix missed definition name change --- Cubical/Data/Cardinal/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Data/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda index 3bb30f186a..1c7371cf0c 100644 --- 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 _ _))