Removed dependency on LehmerCode exporting factorial

anshwad10 · web-flow · commit 630f3bea493a · 2025-02-14T13:26:55.000+05:30
diff --git a/Cubical/Data/FinSet/Cardinality.agda b/Cubical/Data/FinSet/Cardinality.agda
@@ -379,7 +379,7 @@ module _
 module _
   (X : FinSet ℓ ) where
 
-  cardAut : card (_ , isFinSetAut X) ≡ LehmerCode.factorial (card X)
+  cardAut : card (_ , isFinSetAut X) ≡ (card X !)
   cardAut = refl
 
 module _
