Decidable reachability for finite quivers

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

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-⊥-≃ ∣₁