diff --git a/Cubical/Data/FinData/FinSet.agda b/Cubical/Data/FinData/FinSet.agda
new file mode 100644
index 0000000000..af0de436e3
--- /dev/null
+++ b/Cubical/Data/FinData/FinSet.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.FinData.FinSet where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Data.Fin
+  using ()
+  renaming (Fin to Finℕ)
+open import Cubical.Data.FinData
+open import Cubical.Data.Nat as Nat
+  using (ℕ ; _+_)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.SumFin as SumFin
+  using (fzero ; fsuc)
+  renaming (Fin to SumFin)
+open import Cubical.Data.FinSet
+
+open import Cubical.Relation.Nullary
+
+private
+  variable
+    ℓ : Level
+    m n : ℕ
+
+FinFinℕIso : Iso (Fin n) (Finℕ n)
+FinFinℕIso = iso
+  (λ k → toℕ k , toℕ<n k)
+  (uncurry (fromℕ' _))
+  (λ (k , k<n) → Σ≡Prop (λ _ → isProp≤) (toFromId' _ k k<n))
+  (λ k → fromToId' _ k (toℕ<n k))
+
+Fin≃Finℕ : Fin n ≃ Finℕ n
+Fin≃Finℕ = isoToEquiv FinFinℕIso
+
+FinΣ≃ : (n : ℕ) (m : FinVec ℕ n) → Σ (Fin n) (Fin ∘ m) ≃ Fin (foldrFin _+_ 0 m)
+FinΣ≃ 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.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 SumFin.FinData≃SumFin))
+  (SumFin.DecΣ n (P ∘ SumFin.SumFin→FinData) (decP ∘ SumFin.SumFin→FinData))
+
+isFinSetFinData : ∀ {n} → isFinSet (Fin n)
+isFinSetFinData = subst isFinSet (sym SumFin.FinData≡SumFin) isFinSetFin
diff --git a/Cubical/Data/FinSet/Properties.agda b/Cubical/Data/FinSet/Properties.agda
index 34d927ad99..8ece7695aa 100644
--- a/Cubical/Data/FinSet/Properties.agda
+++ b/Cubical/Data/FinSet/Properties.agda
@@ -13,10 +13,13 @@ open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
 open import Cubical.HITs.PropositionalTruncation as Prop
 
 open import Cubical.Data.Nat
+import Cubical.Data.Nat.Order.Recursive as Ord
+import Cubical.Data.Fin as Fin
 open import Cubical.Data.Unit
 open import Cubical.Data.Bool
 open import Cubical.Data.Empty as Empty
 open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
 
 open import Cubical.Data.Fin.Base renaming (Fin to Finℕ)
 open import Cubical.Data.SumFin
@@ -94,3 +97,45 @@ transpFamily :
     {A : Type ℓ}{B : A → Type ℓ'}
   → ((n , e) : isFinOrd A) → (x : A) → B x ≃ B (invEq e (e .fst x))
 transpFamily {B = B} (n , e) x = pathToEquiv (λ i → B (retEq e x (~ i)))
+
+isContr→isFinOrd : ∀ {ℓ} → {A : Type ℓ} →
+  isContr A → isFinOrd A
+isContr→isFinOrd isContrA = 1 , isContr→Equiv isContrA isContrSumFin1
+
+isFinSet⊥ : isFinSet ⊥
+isFinSet⊥ = isFinSetFin
+
+isFinSetLift :
+  {L L' : Level} →
+  {A : Type L} →
+  isFinSet A → isFinSet (Lift {L}{L'} A)
+fst (isFinSetLift {A = A} isFinSetA) = isFinSetA .fst
+snd (isFinSetLift {A = A} isFinSetA) =
+  Prop.elim
+  {P = λ _ → ∥ Lift A ≃ Fin (isFinSetA .fst) ∥₁}
+  (λ [a] → isPropPropTrunc )
+  (λ A≅Fin → ∣ compEquiv (invEquiv (LiftEquiv {A = A})) A≅Fin ∣₁)
+  (isFinSetA .snd)
+
+EquivPresIsFinOrd : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → isFinOrd A → isFinOrd B
+EquivPresIsFinOrd e (_ , p) = _ , compEquiv (invEquiv e) p
+
+isFinOrdFin : ∀ {n} → isFinOrd (Fin n)
+isFinOrdFin {n} = n , (idEquiv (Fin n))
+
+isFinOrd⊥ : isFinOrd ⊥
+fst isFinOrd⊥ = 0
+snd isFinOrd⊥ = idEquiv ⊥
+
+isFinOrdUnit : isFinOrd Unit
+isFinOrdUnit =
+  EquivPresIsFinOrd
+    (isContr→Equiv isContrSumFin1 isContrUnit) isFinOrdFin
+
+takeFirstFinOrd : ∀ {ℓ} → (A : Type ℓ) →
+  (the-ord : isFinOrd A) → 0 Ord.< the-ord .fst → A
+takeFirstFinOrd A (suc n , the-eq) x =
+  the-eq .snd .equiv-proof (Fin→SumFin (Fin.fromℕ≤ 0 n x)) .fst .fst
+
+isFinSet⊤ : isFinSet ⊤
+isFinSet⊤ = 1 , ∣ invEquiv ⊎-IdR-⊥-≃ ∣₁
diff --git a/Cubical/Data/Quiver/Reachability.agda b/Cubical/Data/Quiver/Reachability.agda
new file mode 100644
index 0000000000..7922f22dc7
--- /dev/null
+++ b/Cubical/Data/Quiver/Reachability.agda
@@ -0,0 +1,338 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Quiver.Reachability where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+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
+open import Cubical.Data.Nat hiding (elim)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sum
+
+open import Cubical.Data.Quiver.Base
+
+import Cubical.Data.Equality as Eq
+
+open import Cubical.HITs.PropositionalTruncation as PT hiding (elim ; rec ; map)
+
+open import Cubical.Relation.Nullary.Base
+open import Cubical.Relation.Nullary.Properties
+open import Cubical.Relation.Nullary.DecidablePropositions
+
+private
+  variable
+    ℓ ℓ' : Level
+    n : ℕ
+
+module Reachability {ℓ} {ℓ'}
+  (ob : FinSet ℓ)
+  (Q : QuiverOver ⟨ ob ⟩ ℓ')
+  (isFinSetMor : isFinSet (Q .QuiverOver.mor ))
+  where
+
+  open QuiverOver Q
+
+  data Walk (end : ⟨ ob ⟩) : ⟨ ob ⟩ → ℕ → Type (ℓ-max ℓ ℓ') where
+    nil : Walk end end 0
+    cons : ∀ n (e : mor) → Walk end (cod e) n → Walk end (dom e) (suc n)
+
+  Walk' : (end start : ⟨ ob ⟩) → Type (ℓ-max ℓ ℓ')
+  Walk' end start = Σ[ n ∈ ℕ ] Walk end start n
+
+  trivialWalk→sameEndpoints :
+    (end start : ⟨ ob ⟩) →
+    Walk end start 0 →
+    end ≡ start
+  trivialWalk→sameEndpoints end start nil = refl
+
+  module _
+    (isFinOrdMor : isFinOrd mor) where
+    isFinOrdWalk :
+      ∀ (n : ℕ) →
+      (end start : ⟨ ob ⟩) →
+      isFinOrd (Walk end start n)
+    isFinOrdWalk zero end start =
+      decRec
+        (λ end≡start →
+           1 ,
+           isoToEquiv (
+             iso
+               (λ _ → inl _)
+               (λ { (inl tt) → subst (λ z → Walk end z zero) end≡start nil })
+               (λ { (inl tt) → refl})
+               λ { nil →
+                 cong (λ u → subst (λ z → Walk end z zero) u nil)
+                   (isFinSet→isSet (str ob) end end end≡start refl) ∙
+                 substRefl {B = λ z → Walk end z zero}
+                   Walk.nil }))
+        (λ ¬q≡q' →
+          0 ,
+          uninhabEquiv
+            (λ walk → ¬q≡q' (trivialWalk→sameEndpoints _ _ walk)) (λ x → x)
+            )
+        (isFinSet→Discrete (str ob) end start)
+    isFinOrdWalk (suc n) end start =
+      EquivPresIsFinOrd
+        {A = Σ[ e ∈ mor ] Σ[ src≡start ∈ dom e Eq.≡ start ] Walk end (cod e) n}
+        (isoToEquiv
+          (iso
+            (λ { (e , Eq.refl , walk) → cons n e walk })
+            (λ { (cons .n e walk) → e , Eq.refl , walk })
+            (λ { (cons .n e walk) → refl } )
+            λ { (e , Eq.refl , walk) → refl
+            }
+          ))
+        (isFinOrdΣ mor isFinOrdMor
+          (λ e → _)
+          (λ e → isFinOrdΣ (dom e Eq.≡ start)
+            (decRec
+              (λ src≡start →
+                isContr→isFinOrd ((Eq.pathToEq src≡start) ,
+                (λ { Eq.refl →
+                 cong (Eq.pathToEq)
+                   (isFinSet→isSet (str ob) (dom e) (dom e) src≡start refl) ∙
+                Eq.eqToPath Eq.pathToEq-reflPath })))
+              (λ ¬src≡start → 0 , uninhabEquiv (λ eq → ¬src≡start (Eq.eqToPath eq)) λ x → x)
+              (isFinSet→Discrete (str ob) (dom e) start))
+            _
+            λ { Eq.refl → isFinOrdWalk n end (cod e)}))
+
+    isFinSetWalk :
+      (end start : ⟨ ob ⟩) →
+      (n : ℕ) →
+      isFinSet (Walk end start n)
+    isFinSetWalk end start n = isFinOrd→isFinSet (isFinOrdWalk _ _ _)
+    isSetWalk :
+      (end start : ⟨ ob ⟩) →
+      (n : ℕ) →
+      isSet (Walk end start n)
+    isSetWalk end start n = isFinSet→isSet (isFinSetWalk _ _ _)
+
+  first-edge :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start (suc n)) →
+    mor
+  first-edge (cons _ e walk) = e
+
+  tail :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start (suc n)) →
+    Walk end (cod (first-edge walk)) n
+  tail (cons _ e walk) = walk
+
+  snocWalk :
+    {start : ⟨ ob ⟩} →
+    (e : mor) →
+    Walk (dom e) start n →
+    Walk (cod e) start (suc n)
+  snocWalk e nil = cons 0 e nil
+  snocWalk e (cons n e' walk) = cons (suc n) e' (snocWalk e walk)
+
+  vertices :
+    {end start : ⟨ ob ⟩} →
+    Walk end start n →
+    Fin (suc n) → ⟨ ob ⟩
+  vertices {start = start} walk zero = start
+  vertices (cons n e walk) (suc m) = vertices walk m
+
+  hasUniqueVertices : ∀ {end start : ⟨ ob ⟩} → Walk end start n → Type ℓ
+  hasUniqueVertices walk = isEmbedding (vertices walk)
+
+  hasUniqueVertices→boundedLength :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start n) →
+    hasUniqueVertices walk →
+    n < card ob
+  hasUniqueVertices→boundedLength walk unique =
+    card↪Inequality' (_ , isFinSetFinData) ob (vertices walk) unique
+
+  uniqueVerticesWalk : ∀ (end start : ⟨ ob ⟩) → Type (ℓ-max ℓ ℓ')
+  uniqueVerticesWalk end start =
+    Σ[ n ∈ ℕ ]
+    Σ[ walk ∈ Walk end start n ] hasUniqueVertices walk
+
+  tailUniqueVertices :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start (suc n)) →
+    hasUniqueVertices walk →
+    hasUniqueVertices (tail walk)
+  tailUniqueVertices (cons _ e walk) uniq =
+    isEmbedding-∘ uniq (injEmbedding isSetFin injSucFin)
+
+  dec-hasUniqueVertices :
+    ∀ {end start : ⟨ ob ⟩} → (walk : Walk end start n) →
+      Dec (hasUniqueVertices walk)
+  dec-hasUniqueVertices nil =
+    yes (injEmbedding (isFinSet→isSet (str ob))
+      (λ { {zero} {zero} → λ _ → refl }))
+  dec-hasUniqueVertices (cons n e walk) =
+    decRec
+      (λ (k , p) → no (λ x →
+        FD.znots (x zero (suc k) .equiv-proof (sym p) .fst .fst)))
+      (λ ¬repeatFirst →
+        decRec
+          (λ uniqWalk → yes
+            (λ j k →
+              injEmbedding
+                (isFinSet→isSet (str ob))
+                (λ {
+                  {zero} {zero} → λ _ → refl
+                ; {zero} {suc b} →
+                  λ dom≡vert →
+                    ⊥.rec (¬repeatFirst (b , (sym dom≡vert)))
+                ; {suc a} {zero} →
+                  λ dom≡vert → ⊥.rec (¬repeatFirst (a , dom≡vert))
+                ; {suc a} {suc b} → λ verts≡ →
+                  decRec
+                    (λ a≡b → cong suc a≡b)
+                    (λ ¬a≡b →
+                      ⊥.rec
+                        (¬a≡b (uniqWalk a b .equiv-proof verts≡ .fst .fst)))
+                    (discreteFin a b)
+                })
+                j
+                k)
+          )
+          (λ ¬uniqWalk → no (λ x → ¬uniqWalk (tailUniqueVertices _ x)))
+          (dec-hasUniqueVertices walk)
+      )
+      (DecΣ (suc n) (λ k → vertices walk k ≡ dom e)
+      (λ k → isFinSet→Discrete (str ob) (vertices walk k) (dom e)))
+
+
+  drop : {end start : ⟨ ob ⟩} →
+    (walk : Walk end start n) →
+    (k : Fin (suc n)) →
+    Σ[ m ∈ ℕ ] Walk end (vertices walk k) m
+  drop walk zero = _ , walk
+  drop (cons n e walk) (suc k) = drop walk k
+
+  dropPreservesUnique :
+    {end start : ⟨ ob ⟩} →
+    (uniqWalk : uniqueVerticesWalk end start) →
+    (k : Fin (suc (uniqWalk .fst))) →
+    hasUniqueVertices (drop (uniqWalk .snd .fst) k .snd)
+  dropPreservesUnique uniqWalk zero = uniqWalk .snd .snd
+  dropPreservesUnique (n , cons n-1 e walk , uniq) (suc k) =
+    dropPreservesUnique
+      (n-1 ,
+      (walk , tailUniqueVertices (cons n-1 e walk) uniq)) k
+
+  UniqueWalk : ∀ (end start : ⟨ ob ⟩) → Type _
+  UniqueWalk end start =
+    Σ[ n ∈ Fin (card ob) ]
+    Σ[ walk ∈ Walk end start (toℕ n) ] hasUniqueVertices walk
+
+
+  makeUnique :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start n) →
+    uniqueVerticesWalk end start
+  makeUnique nil =
+    0 ,
+    nil ,
+    injEmbedding
+      (isFinSet→isSet (str ob))
+      (λ _ → isContr→isProp isContrFin1 _ _)
+  makeUnique {end = end}(cons n e walk) =
+    let new-vert = dom e in
+    let new-edge = e in
+    let n' , walk' , uniq = makeUnique walk in
+    decRec
+      -- There is a repeated vertex
+      (λ (m , p) →
+        let n'' , walk'' = drop walk' m in
+        let uniq' = dropPreservesUnique (n' , (walk' , uniq)) m in
+        n'' ,
+        subst (λ z → Σ[ w ∈ Walk end z n'' ] hasUniqueVertices w) p (walk'' , uniq'))
+      -- There is no repeated vertex
+      (λ ¬ΣnewVert →
+        suc n' ,
+        (cons n' new-edge walk' ,
+        injEmbedding
+          (isFinSet→isSet (str ob))
+              λ { {zero} {zero} p → refl
+                ; {zero} {suc j} p → ⊥.rec (¬ΣnewVert (j , (sym p)))
+                ; {suc i} {zero} p → ⊥.rec (¬ΣnewVert (i , p))
+                ; {suc i} {suc j} p → congS suc $ isEmbedding→Inj uniq i j p
+                }
+          )
+      )
+      (DecΣ
+        (suc n')
+        (λ k → vertices walk' k ≡ new-vert)
+        (λ k → isFinSet→Discrete (str ob) (vertices walk' k) new-vert))
+
+  Walk→UniqueWalk :
+    {end start : ⟨ ob ⟩} →
+    (walk : Walk end start n) →
+    UniqueWalk end start
+  Walk→UniqueWalk {end = end}{start = start} walk =
+    let m , walk' , uniq = makeUnique walk in
+    let bound = hasUniqueVertices→boundedLength walk' uniq in
+    let to-and-fro = sym (toFromId' (card ob) m bound) in
+    fromℕ' (card ob) m bound ,
+      subst
+        (λ n' → Σ[ walk ∈ Walk end start n' ] hasUniqueVertices walk)
+          to-and-fro (walk' , uniq)
+
+  Reachable PathReachable : ⟨ ob ⟩ → ⟨ ob ⟩ → Type _
+  Reachable end start =
+    PT.∥ Σ[ n ∈ ℕ ] Walk end start n  ∥₁
+  PathReachable end start =
+    PT.∥ UniqueWalk end start ∥₁
+
+  PathReachable≃Reachable :
+    (end start : ⟨ ob ⟩) → PathReachable end start ≃ Reachable end start
+  PathReachable≃Reachable end start =
+    propBiimpl→Equiv isPropPropTrunc isPropPropTrunc
+      (PT.map (λ gp → (toℕ (gp .fst)) , (gp .snd .fst)))
+      (PT.map (λ (n , gw) → Walk→UniqueWalk gw))
+
+  isFinSetHasUniqueVertices :
+    {end start : ⟨ ob ⟩} →
+    (gw : Walk end start n) → isFinSet (hasUniqueVertices gw)
+  isFinSetHasUniqueVertices gw =
+    isFinSetIsEmbedding (_ , isFinSetFinData) ob (vertices gw)
+
+  module _
+    (isFinOrdMor : isFinOrd mor)
+    (end start : ⟨ ob ⟩)
+    where
+
+    isFinOrdUniqueWalk : isFinOrd (UniqueWalk end start)
+    isFinOrdUniqueWalk =
+      isFinOrdΣ
+        (Fin (ob .snd .fst))
+        ((card ob) , SumFin.FinData≃SumFin)
+        (λ n → Σ-syntax (Walk end start (toℕ n)) hasUniqueVertices)
+        (λ m → isFinOrdΣ
+          (Walk end start (toℕ m))
+          (isFinOrdWalk isFinOrdMor (toℕ m) end start)
+          hasUniqueVertices
+          (λ walk → DecProp→isFinOrd ((_ , isPropIsEmbedding) , dec-hasUniqueVertices walk)))
+    isFinSetUniqueWalk : isFinSet (UniqueWalk end start)
+    isFinSetUniqueWalk =
+      isFinOrd→isFinSet isFinOrdUniqueWalk
+
+    DecPathReachable : Dec (PathReachable end start)
+    DecPathReachable = isFinSet→Dec∥∥ isFinSetUniqueWalk
+
+    DecReachable : Dec (Reachable end start)
+    DecReachable =
+      EquivPresDec
+        (PathReachable≃Reachable end start)
+        DecPathReachable
+
+  Reachable-is-reflexive : (u : ⟨ ob ⟩) → Reachable u u
+  Reachable-is-reflexive u = ∣ 0 , nil ∣₁
diff --git a/Cubical/Data/SumFin/Properties.agda b/Cubical/Data/SumFin/Properties.agda
index ad5077200c..2bfc9cff19 100644
--- a/Cubical/Data/SumFin/Properties.agda
+++ b/Cubical/Data/SumFin/Properties.agda
@@ -12,9 +12,10 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Unit
 open import Cubical.Data.Bool hiding (_≤_)
-open import Cubical.Data.Nat
-open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat as Nat
+open import Cubical.Data.Nat.Order as Ord
 import Cubical.Data.Fin as Fin
+import Cubical.Data.FinData as FinData
 import Cubical.Data.Fin.LehmerCode as LehmerCode
 open import Cubical.Data.SumFin.Base as SumFin
 open import Cubical.Data.Sum as ⊎
@@ -27,7 +28,7 @@ open import Cubical.Relation.Nullary
 private
   variable
     ℓ : Level
-    k : ℕ
+    n m k : ℕ
 
 SumFin→Fin : Fin k → Fin.Fin k
 SumFin→Fin = SumFin.elim (λ {k} _ → Fin.Fin k) Fin.fzero Fin.fsuc
@@ -270,3 +271,48 @@ SumFin≃≃ _ =
   ⋆ LehmerCode.lehmerEquiv
   ⋆ LehmerCode.lehmerFinEquiv
   ⋆ invEquiv (SumFin≃Fin _)
+
+-- Relate SumFin and FinData
+
+FinData→SumFin : FinData.Fin n → SumFin.Fin n
+FinData→SumFin = FinData.elim (λ {n} _ → SumFin.Fin n) fzero fsuc
+
+SumFin→FinData : SumFin.Fin n → FinData.Fin n
+SumFin→FinData = SumFin.elim (λ {n} _ → FinData.Fin n) FinData.zero FinData.suc
+
+FinDataSumFinIso : Iso (FinData.Fin n) (SumFin.Fin n)
+FinDataSumFinIso = iso FinData→SumFin SumFin→FinData
+  (SumFin.elim (λ fn → FinData→SumFin (SumFin→FinData fn) ≡ fn) refl (cong fsuc))
+  (FinData.elim (λ fn → SumFin→FinData (FinData→SumFin fn) ≡ fn) refl (cong FinData.suc))
+
+FinData≃SumFin : FinData.Fin n ≃ SumFin.Fin n
+FinData≃SumFin = isoToEquiv FinDataSumFinIso
+
+≡→FinData≃SumFin : m ≡ n → FinData.Fin m ≃ SumFin.Fin n
+≡→FinData≃SumFin {m} = J (λ n p → FinData.Fin m ≃ SumFin.Fin n) FinData≃SumFin
+
+FinData≡SumFin : FinData.Fin n ≡ SumFin.Fin n
+FinData≡SumFin = ua FinData≃SumFin
+
+DecΣ :
+  (n : ℕ) →
+  (P : Fin n → Type ℓ) →
+  ((k : Fin n) → Dec (P k)) →
+  Dec (Σ (Fin n) P)
+DecΣ = Nat.elim
+  (λ _ _ → no fst)
+  (λ n ih P decP →
+    decRec
+    (yes ∘ (_ ,_))
+    (λ ¬Pzero →
+      mapDec
+      (λ (k , Pk) → (fsuc k , Pk))
+      (λ ¬Psuc →
+        λ { (fzero , Pzero) → ¬Pzero Pzero
+          ; (fsuc k , Pk) → ¬Psuc (k , Pk)
+          })
+      (ih (P ∘ fsuc) (decP ∘ fsuc))
+    )
+    (decP fzero)
+  )
+
diff --git a/Cubical/Relation/Nullary/DecidablePropositions.agda b/Cubical/Relation/Nullary/DecidablePropositions.agda
index 69b7ec8506..3f2b029c88 100644
--- a/Cubical/Relation/Nullary/DecidablePropositions.agda
+++ b/Cubical/Relation/Nullary/DecidablePropositions.agda
@@ -3,10 +3,14 @@ module Cubical.Relation.Nullary.DecidablePropositions where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
 
 open import Cubical.Data.Bool
 open import Cubical.Data.Sigma
+open import Cubical.Data.FinSet
+open import Cubical.Data.Sum
+open import Cubical.Data.Empty
 
 open import Cubical.Relation.Nullary.Base
 open import Cubical.Relation.Nullary.Properties
@@ -47,3 +51,18 @@ isPropIsDecProp p q =
 isDecPropRespectEquiv : {P : Type ℓ} {Q : Type ℓ'}
   → P ≃ Q → isDecProp Q → isDecProp P
 isDecPropRespectEquiv e (t , e') = t , e ⋆ e'
+
+DecProp→isFinOrd :
+  ∀ {ℓ} → (A : DecProp ℓ) → isFinOrd (A .fst .fst)
+DecProp→isFinOrd A =
+  decRec
+    (λ a →
+      1 ,
+      isoToEquiv
+      (iso
+        (λ _ → inl _)
+        (λ { (inl tt) → a ; (inr ()) })
+        (λ { (inl tt) → refl ; (inr ()) })
+        (λ a → A .fst .snd _ _)))
+    (λ ¬a → 0 , uninhabEquiv ¬a (λ x → x))
+    (A .snd)