Remove duplicated code

Author: stschaef

Cubical/Data/FinData/FinSet.agda

@@ -27,26 +27,6 @@ private
     ℓ : Level
     m n : ℕ
 
-Fin→SumFin : Fin n → SumFin.Fin n
-Fin→SumFin = elim (λ {n} _ → SumFin n) fzero fsuc
-
-SumFin→Fin : SumFin.Fin n → Fin n
-SumFin→Fin = SumFin.elim (λ {n} _ → Fin n) zero suc
-
-FinSumFinIso : Iso (Fin n) (SumFin n)
-FinSumFinIso = iso Fin→SumFin SumFin→Fin
-  (SumFin.elim (λ fn → Fin→SumFin (SumFin→Fin fn) ≡ fn) refl (cong fsuc))
-  (elim (λ fn → SumFin→Fin (Fin→SumFin fn) ≡ fn) refl (cong suc))
-
-Fin≃SumFin : Fin n ≃ SumFin n
-Fin≃SumFin = isoToEquiv FinSumFinIso
-
-≡→Fin≃SumFin : m ≡ n → Fin m ≃ SumFin n
-≡→Fin≃SumFin {m} = J (λ n p → Fin m ≃ SumFin n) Fin≃SumFin
-
-Fin≡SumFin : Fin n ≡ SumFin n
-Fin≡SumFin = ua Fin≃SumFin
-
 FinFinℕIso : Iso (Fin n) (Finℕ n)
 FinFinℕIso = iso
   (λ k → toℕ k , toℕ<n k)
@@ -59,20 +39,20 @@ Fin≃Finℕ = isoToEquiv FinFinℕIso
 
 FinΣ≃ : (n : ℕ) (m : FinVec ℕ n) → Σ (Fin n) (Fin ∘ m) ≃ Fin (foldrFin _+_ 0 m)
 FinΣ≃ n m =
-  Σ-cong-equiv Fin≃SumFin (λ fn → ≡→Fin≃SumFin
-    (congS m (sym (retIsEq (Fin≃SumFin .snd) fn))))
-  ∙ₑ SumFin.SumFinΣ≃ n (m ∘ SumFin→Fin)
-  ∙ₑ invEquiv (≡→Fin≃SumFin (sum≡ n m))
+  Σ-cong-equiv SumFin.FinData≃SumFin (λ fn → SumFin.≡→FinData≃SumFin
+    (congS m (sym (retIsEq (SumFin.FinData≃SumFin .snd) fn))))
+  ∙ₑ SumFin.SumFinΣ≃ n (m ∘ SumFin.SumFin→FinData)
+  ∙ₑ invEquiv (SumFin.≡→FinData≃SumFin (sum≡ n m))
   where
   sum≡ : (n : ℕ) (m : FinVec ℕ n) →
-    foldrFin _+_ 0 m ≡ SumFin.totalSum (m ∘ SumFin→Fin)
+    foldrFin _+_ 0 m ≡ SumFin.totalSum (m ∘ SumFin.SumFin→FinData)
   sum≡ = Nat.elim (λ _ → refl) λ n x m → congS (m zero +_) (x (m ∘ suc))
 
 DecΣ : (n : ℕ) →
   (P : FinVec (Type ℓ) n) → (∀ k → Dec (P k)) → Dec (Σ (Fin n) P)
 DecΣ n P decP = EquivPresDec
-  (Σ-cong-equiv-fst (invEquiv Fin≃SumFin))
-  (SumFin.DecΣ n (P ∘ SumFin→Fin) (decP ∘ SumFin→Fin))
+  (Σ-cong-equiv-fst (invEquiv SumFin.FinData≃SumFin))
+  (SumFin.DecΣ n (P ∘ SumFin.SumFin→FinData) (decP ∘ SumFin.SumFin→FinData))
 
 isFinSetFinData : ∀ {n} → isFinSet (Fin n)
-isFinSetFinData = subst isFinSet (sym Fin≡SumFin) isFinSetFin
+isFinSetFinData = subst isFinSet (sym SumFin.FinData≡SumFin) isFinSetFin

Cubical/Data/Quiver/Reachability.agda

@@ -11,6 +11,7 @@ open import Cubical.Functions.Embedding
 open import Cubical.Data.Empty as ⊥ hiding (elim ; rec)
 open import Cubical.Data.FinData as FD
 open import Cubical.Data.FinData.FinSet
+import Cubical.Data.SumFin as SumFin
 open import Cubical.Data.FinSet
 open import Cubical.Data.FinSet.Cardinality
 open import Cubical.Data.FinSet.Constructors
@@ -313,7 +314,7 @@ module Reachability {ℓ} {ℓ'}
     isFinOrdUniqueWalk =
       isFinOrdΣ
         (Fin (ob .snd .fst))
-        ((card ob) , Fin≃SumFin)
+        ((card ob) , SumFin.FinData≃SumFin)
         (λ n → Σ-syntax (Walk end start (toℕ n)) hasUniqueVertices)
         (λ m → isFinOrdΣ
           (Walk end start (toℕ m))