a few minor utility functions

Cubical/Data/Bool/Properties.agda

@@ -427,3 +427,19 @@ Iso.leftInv Iso-Bool→∙Bool-Bool f = Σ≡Prop (λ _ → isSetBool _ _) (help
       ; true → (λ j → Bool→Bool→∙Bool (p j) .fst true) ∙ sym (snd f)}
   help true p = (λ j → Bool→Bool→∙Bool (p j) .fst)
               ∙ funExt λ { false → sym p ; true → sym (snd f)}
+
+ΣBool : (b : Bool) (c : (Bool→Type b) → Bool) → Bool
+ΣBool false c = false
+ΣBool true c = c tt
+
+ΣBoolΣIso : {b : Bool} {c : (Bool→Type b) → Bool} →
+  Iso (Bool→Type (ΣBool b c)) (Σ[ z ∈ Bool→Type b ] Bool→Type (c z))
+
+Iso.fun (ΣBoolΣIso {true}) x = tt , x
+Iso.inv (ΣBoolΣIso {true}) x = snd x
+Iso.leftInv (ΣBoolΣIso {true}) _ = refl
+Iso.rightInv (ΣBoolΣIso {true}) _ = refl
+
+ΣBool≃Σ : {b : Bool} {c : (Bool→Type b) → Bool} →
+  (Bool→Type (ΣBool b c)) ≃ (Σ[ z ∈ Bool→Type b ] Bool→Type (c z))
+ΣBool≃Σ = isoToEquiv ΣBoolΣIso

Cubical/Data/List/FinData.agda

@@ -3,9 +3,12 @@ module Cubical.Data.List.FinData where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.List
 open import Cubical.Data.FinData
 open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sigma.Properties
 open import Cubical.Data.Nat
 
 variable
@@ -34,6 +37,18 @@ lookup-tabulate : ∀ n → (^a : Fin n → A)
 lookup-tabulate (suc n) ^a i zero = ^a zero
 lookup-tabulate (suc n) ^a i (suc p) = lookup-tabulate n (^a ∘ suc) i p
 
+open Iso
+
+lookup-tabulate-iso : (A : Type ℓ) → Iso (List A) (Σ[ n ∈ ℕ ] (Fin n → A))
+fun (lookup-tabulate-iso A) xs = (length xs) , lookup xs
+inv (lookup-tabulate-iso A) (n , f) = tabulate n f
+leftInv (lookup-tabulate-iso A) = tabulate-lookup
+rightInv (lookup-tabulate-iso A) (n , f) =
+  ΣPathP ((length-tabulate n f) , lookup-tabulate n f)
+
+lookup-tabulate-equiv : (A : Type ℓ) → List A ≃ (Σ[ n ∈ ℕ ] (Fin n → A))
+lookup-tabulate-equiv A = isoToEquiv (lookup-tabulate-iso A)
+
 lookup-map : ∀ (f : A → B) (xs : List A)
   → (p0 : Fin (length (map f xs)))
   → (p1 : Fin (length xs))

Cubical/HITs/Nullification/Properties.agda

@@ -28,7 +28,7 @@ open isPathSplitEquiv
 
 private
   variable
-    ℓα ℓs ℓ ℓ' : Level
+    ℓα ℓs ℓ ℓ' ℓ'' : Level
     A : Type ℓα
     S : A → Type ℓs
     X : Type ℓ
@@ -250,3 +250,29 @@ secCong (SeparatedAndInjective→Null X sep inj α) x y =
   fst s ∘ funExt⁻ , λ p i j α → snd s (funExt⁻ p) i α j
   where
     s = sec (sep x y α)
+
+generatorsConnected : {A : Type ℓα} (S : A → Type ℓ) →
+  (a : A) → isContr (Null S (S a))
+generatorsConnected S a = (hub a ∣_∣) ,
+  elim (λ _ → isNull≡ (isNull-Null S)) (spoke a ∣_∣)
+
+nullMap : {A : Type ℓα} (S : A → Type ℓ) →
+  {X : Type ℓ'} {Y : Type ℓ''} → (X → Y) → Null S X → Null S Y
+nullMap S f ∣ x ∣ = ∣ f x ∣
+nullMap S f (hub α g) = hub α (λ z → nullMap S f (g z))
+nullMap S f (spoke α g s i) = spoke α (λ z → nullMap S f (g z)) s i
+nullMap S f (≡hub p i) = ≡hub (λ z j → nullMap S f (p z j)) i
+nullMap S f (≡spoke p s i i₁) = ≡spoke (λ z j → nullMap S f (p z j)) s i i₁
+
+nullPreservesIso : {A : Type ℓα} (S : A → Type ℓ) → {X : Type ℓ'} →
+  {Y : Type ℓ''} → Iso X Y → Iso (Null S X) (Null S Y)
+Iso.fun (nullPreservesIso S e) = nullMap S (Iso.fun e)
+Iso.inv (nullPreservesIso S e) = nullMap S (Iso.inv e)
+Iso.leftInv (nullPreservesIso S e) =
+  elim (λ _ → isNull≡ (isNull-Null S)) (λ x → cong ∣_∣ (Iso.leftInv e x))
+Iso.rightInv (nullPreservesIso S e) =
+  elim (λ _ → isNull≡ (isNull-Null S)) (λ y → cong ∣_∣ (Iso.rightInv e y))
+
+nullPreservesEquiv : {A : Type ℓα} (S : A → Type ℓ) → {X : Type ℓ'} →
+  {Y : Type ℓ''} → X ≃ Y → Null S X ≃ Null S Y
+nullPreservesEquiv S {X = X} {Y = Y} e = isoToEquiv (nullPreservesIso S (equivToIso e))

Cubical/Relation/Nullary/Properties.agda

@@ -24,7 +24,7 @@ open import Cubical.HITs.PropositionalTruncation.Base
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
     A B : Type ℓ
     P : A -> Type ℓ
 
@@ -62,6 +62,13 @@ Stable× As Bs e = λ where
   .fst → As λ k → e (k ∘ fst)
   .snd → Bs λ k → e (k ∘ snd)
 
+StableΣ : ∀ {A : Type ℓ} {P : A → Type ℓ'} →
+  Stable A → isProp A → ((a : A) → Stable (P a)) → Stable (Σ A P)
+StableΣ {P = P} As Aprop Ps e =
+  let a = (As (λ notA → e (λ (a , _) → notA a))) in
+  a ,
+  Ps a λ notPa → e (λ (a' , p) → notPa (subst P (Aprop a' a) p))
+
 fromYes : A → Dec A → A
 fromYes _ (yes a) = a
 fromYes a (no _) = a