Move factorial from Cubical.Data.Fin.LehmerCode to Cubical.Data.Nat.Properties (#1184)

* Update LehmerCode.agda

* Update Properties.agda

add `factorial` here

* Update LehmerCode.agda

made it export `factorial` so nothing else in the library that depends on `factorial` being exported breaks

* Removed dependency on LehmerCode exporting `factorial`

* Removed dependency on LehmerCode exporting `factorial`

* Removed dependency on LehmerCode exporting `factorial`

* Remove the public export of `factorial` from LehmerCode.agda

Author: anshwad10

Cubical/Data/Fin/LehmerCode.agda

@@ -191,10 +191,6 @@ encode = equivFun lehmerEquiv
 decode : LehmerCode n → Fin n ≃ Fin n
 decode = invEq lehmerEquiv
 
--- Use the one in Cubical.Data.Nat.Properties instead
-factorial : ℕ → ℕ
-factorial = _!
-
 lehmerFinEquiv : LehmerCode n ≃ Fin (n !)
 lehmerFinEquiv {zero} = isContr→Equiv isContrLehmerZero isContrFin1
 lehmerFinEquiv {suc n} = _ ≃⟨ invEquiv lehmerSucEquiv ⟩

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 _

Cubical/Data/FinSet/Constructors.agda

@@ -168,7 +168,7 @@ module _
   (X : FinSet ℓ) where
 
   isFinSetAut : isFinSet (X .fst ≃ X .fst)
-  isFinSetAut = LehmerCode.factorial (card X) ,
+  isFinSetAut = card X ! ,
     Prop.map (λ p → isFinOrd≃ (X .fst) (card X , p) .snd) (X .snd .snd)
 
   isFinSetTypeAut : isFinSet (X .fst ≡ X .fst)

Cubical/Data/Nat/Properties.agda

@@ -266,12 +266,14 @@ n∸n (suc n) = n∸n n
 ∸-distribʳ zero    (suc n) k = sym (zero∸ (k + n · k))
 ∸-distribʳ (suc m) (suc n) k = ∸-distribʳ m n k ∙ sym (∸-cancelˡ k (m · k) (n · k))
 
-
+infix 6 _!
+infix 7 _choose_
 
 -- factorial:
-_! : ℕ → ℕ
+_! factorial : ℕ → ℕ
 zero ! = 1
-suc n ! = (suc n) · (n !)
+suc n ! = suc n · (n !)
+factorial = _!
 
 --binomial coefficient:
 _choose_ : ℕ → ℕ → ℕ

Cubical/Data/SumFin/Properties.agda

@@ -264,7 +264,7 @@ isProp→Fin≤1 (suc (suc n)) p = ⊥.rec (fzero≠fone (p fzero (fsuc fzero)))
 
 -- automorphisms of SumFin
 
-SumFin≃≃ : (n : ℕ) → (Fin n ≃ Fin n) ≃ Fin (LehmerCode.factorial n)
+SumFin≃≃ : (n : ℕ) → (Fin n ≃ Fin n) ≃ Fin (n !)
 SumFin≃≃ _ =
     equivComp (SumFin≃Fin _) (SumFin≃Fin _)
   ⋆ LehmerCode.lehmerEquiv