typo again ;)

agda · Mar 26, 2022 · 6e15312 · 6e15312
1 parent 2f1c902
commit 6e15312
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Data/FinSet/Cardinality.agda b/Cubical/Data/FinSet/Cardinality.agda
@@ -161,7 +161,7 @@ module _
 
 {- formulae about cardinality -}
 
--- results to be used in diProp.rect induction on FinSet
+-- results to be used in direct induction on FinSet
 
 card𝟘 : card (𝟘 {ℓ}) ≡ 0
 card𝟘 {ℓ = ℓ} = isEmpty→card≡0 (𝟘 {ℓ}) (Empty.rec*)