Various functions that I found useful (#951)

* added various functions that I found useful

* allow multiple universe levels in definition of JDep

* remove unecessary implicit arguments from JDep

Author: awswan

Cubical/Data/Nat/Order.agda

@@ -252,9 +252,15 @@ min-≤-right {suc m} {suc n} = suc-≤-suc min-≤-right
 ... | yes m≤n = yes (suc-≤-suc m≤n)
 ... | no m≰n = no λ m+1≤n+1 → m≰n (pred-≤-pred m+1≤n+1 )
 
+≤Stable : ∀ m n → Stable (m ≤ n)
+≤Stable m n = Dec→Stable (≤Dec m n)
+
 <Dec : ∀ m n → Dec (m < n)
 <Dec m n = ≤Dec (suc m) n
 
+<Stable : ∀ m n → Stable (m < n)
+<Stable m n = Dec→Stable (<Dec m n)
+
 Trichotomy-suc : Trichotomy m n → Trichotomy (suc m) (suc n)
 Trichotomy-suc (lt m<n) = lt (suc-≤-suc m<n)
 Trichotomy-suc (eq m=n) = eq (cong suc m=n)

Cubical/Data/Nat/Properties.agda

@@ -127,6 +127,9 @@ discreteℕ (suc m) (suc n) with discreteℕ m n
 ... | yes p = yes (cong suc p)
 ... | no p = no (λ x → p (injSuc x))
 
+separatedℕ : Separated ℕ
+separatedℕ = Discrete→Separated discreteℕ
+
 isSetℕ : isSet ℕ
 isSetℕ = Discrete→isSet discreteℕ
 

Cubical/Data/Sigma/Properties.agda

@@ -446,3 +446,13 @@ module _
 
     fiberProjEquiv : B a ≃ fiber proj a
     fiberProjEquiv = isoToEquiv fiberProjIso
+
+separatedΣ : Separated A → ((a : A) → Separated (B a)) → Separated (Σ A B)
+separatedΣ {B = B} sepA sepB (a , b) (a' , b') p = ΣPathTransport→PathΣ _ _ (pA , pB)
+  where
+    pA : a ≡ a'
+    pA = sepA a a' (λ q → p (λ r → q (cong fst r)))
+
+    pB : subst B pA b ≡ b'
+    pB = sepB _ _ _ (λ q → p (λ r → q (cong (λ r' → subst B r' b)
+                                (Separated→isSet sepA _ _ pA (cong fst r)) ∙ snd (PathΣ→ΣPathTransport _ _ r))))

Cubical/Data/Sum/Properties.agda

@@ -10,6 +10,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Empty
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
+open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Sum.Base
 
@@ -107,6 +108,14 @@ isGroupoid⊎ = isOfHLevel⊎ 1
 is2Groupoid⊎ : is2Groupoid A → is2Groupoid B → is2Groupoid (A ⊎ B)
 is2Groupoid⊎ = isOfHLevel⊎ 2
 
+discrete⊎ : Discrete A → Discrete B → Discrete (A ⊎ B)
+discrete⊎ decA decB (inl a) (inl a') =
+  mapDec (cong inl) (λ p q → p (isEmbedding→Inj isEmbedding-inl _ _ q)) (decA a a')
+discrete⊎ decA decB (inl a) (inr b') = no (λ p → lower (⊎Path.encode (inl a) (inr b') p))
+discrete⊎ decA decB (inr b) (inl a') = no ((λ p → lower (⊎Path.encode (inr b) (inl a') p)))
+discrete⊎ decA decB (inr b) (inr b') =
+  mapDec (cong inr) (λ p q → p (isEmbedding→Inj isEmbedding-inr _ _ q)) (decB b b')
+
 ⊎Iso : Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
 fun (⊎Iso iac ibd) (inl x) = inl (iac .fun x)
 fun (⊎Iso iac ibd) (inr x) = inr (ibd .fun x)

Cubical/Foundations/HLevels.agda

@@ -576,6 +576,9 @@ isGroupoidHSet = isOfHLevelTypeOfHLevel 2
 isOfHLevelLift : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n A → isOfHLevel n (Lift {j = ℓ'} A)
 isOfHLevelLift n = isOfHLevelRetract n lower lift λ _ → refl
 
+isOfHLevelLower : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} → isOfHLevel n (Lift {j = ℓ'} A) → isOfHLevel n A
+isOfHLevelLower n = isOfHLevelRetract n lift lower λ _ → refl
+
 ----------------------------
 
 -- More consequences of isProp and isContr

Cubical/Foundations/Prelude.agda

@@ -347,8 +347,7 @@ module _ (P : ∀ y → x ≡ y → Type ℓ') (d : P x refl) where
 
 -- Multi-variable versions of J
 
-module _ {x : A}
-  {B : A → Type ℓ''} {b : B x}
+module _ {b : B x}
   (P : (y : A) (p : x ≡ y) (z : B y) (q : PathP (λ i → B (p i)) b z) → Type ℓ'')
   (d : P _ refl _ refl) where
 

Cubical/HITs/Nullification/Properties.agda

@@ -10,6 +10,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.PathSplit
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Univalence
+open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Modalities.Modality
 
@@ -22,6 +23,34 @@ open import Cubical.HITs.Nullification.Base
 open Modality
 open isPathSplitEquiv
 
+private
+  variable
+    ℓα ℓs ℓ ℓ' : Level
+
+isNull≡ : {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} (nX : isNull S X) {x y : X} → isNull S (x ≡ y)
+isNull≡ {A = A} {S = S} nX {x = x} {y = y} α =
+  fromIsEquiv (λ p _ i → p i)
+              (isEquiv[equivFunA≃B∘f]→isEquiv[f] (λ p _ → p) funExtEquiv (isEquivCong (const , toIsEquiv _ (nX α))))
+
+isNullΠ : {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : X → Type ℓ'} → ((x : X) → isNull S (Y x)) →
+                 isNull S ((x : X) → Y x)
+isNullΠ {S = S} {X = X} {Y = Y} nY α = fromIsEquiv _ (snd e)
+  where
+    flipIso : Iso ((x : X) → S α → Y x) (S α → (x : X) → Y x)
+    Iso.fun flipIso f = flip f
+    Iso.inv flipIso f = flip f
+    Iso.rightInv flipIso f = refl
+    Iso.leftInv flipIso f = refl
+
+    e : ((x : X) → Y x) ≃ (S α → ((x : X) → Y x))
+    e =
+      ((x : X) → Y x)
+        ≃⟨ equivΠCod (λ x → const , (toIsEquiv _ (nY x α))) ⟩
+      ((x : X) → (S α → Y x))
+        ≃⟨ isoToEquiv flipIso ⟩
+      (S α → ((x : X) → Y x))
+        ■
+
 rec : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'}
       → (nB : isNull S Y) → (X → Y) → Null S X → Y
 rec nB g ∣ x ∣ = g x
@@ -83,6 +112,26 @@ module _ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type
                      (λ i → elim nY g (p s i))
           q₂ j i = toPathP⁻ (λ j → Y (≡spoke p s j i)) (λ j → q₁ j i) j
 
+NullRecIsPathSplitEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} → (isNull S Y) →
+                          isPathSplitEquiv {A = (Null S X) → Y} (λ f → f ∘ ∣_∣)
+sec (NullRecIsPathSplitEquiv nY) = rec nY , λ _ → refl
+secCong (NullRecIsPathSplitEquiv nY) f f' = (λ p → funExt (elim (λ _ → isNull≡ nY) (funExt⁻ p))) , λ _ → refl
+
+NullRecIsEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} →  (isNull S Y) →
+                          isEquiv {A = (Null S X) → Y} (λ f → f ∘ ∣_∣)
+NullRecIsEquiv nY = toIsEquiv _ (NullRecIsPathSplitEquiv nY)
+
+NullRecEquiv : ∀ {ℓα ℓs ℓ ℓ'} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} {Y : Type ℓ'} → (isNull S Y) →
+                          ((Null S X) → Y) ≃ (X → Y)
+NullRecEquiv nY = (λ f → f ∘ ∣_∣) , (NullRecIsEquiv nY)
+
+
+NullPreservesProp : ∀ {ℓα ℓs ℓ} {A : Type ℓα} {S : A → Type ℓs} {X : Type ℓ} →
+                    (isProp X) → isProp (Null S X)
+
+NullPreservesProp {S = S} pX u = elim (λ v' → isNull≡ (isNull-Null S))
+  (λ y → elim (λ u' → isNull≡ (isNull-Null S) {x = u'}) (λ x → cong ∣_∣ (pX x y)) u)
+
 -- nullification is a modality
 
 NullModality : ∀ {ℓα ℓs ℓ} {A : Type ℓα} (S : A → Type ℓs) → Modality (ℓ-max ℓ (ℓ-max ℓα ℓs))

Cubical/Modalities/Modality.agda

@@ -12,6 +12,7 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv.Properties
 
 record Modality ℓ : Type (ℓ-suc ℓ) where
   field
@@ -158,3 +159,10 @@ record Modality ℓ : Type (ℓ-suc ℓ) where
 
           r : (x : Σ A B) → η-inv (η x) ≡ x
           r x = (λ i → h (η x) , p x i) ∙ (almost x)
+
+  isModal≡ : {A : Type ℓ} → (isModal A) → {x y : A} → (isModal (x ≡ y))
+  isModal≡ A-modal = equivPreservesIsModal (invEquiv (congEquiv (η , (isModalToIsEquiv A-modal)))) (◯-=-isModal _ _)
+
+  ◯-preservesProp : {A : Type ℓ} → (isProp A) → (isProp (◯ A))
+  ◯-preservesProp pA u = ◯-elim (λ z → ◯-=-isModal _ _)
+                         λ b → ◯-elim (λ x → ◯-=-isModal _ _) (λ a → cong η (pA a b)) u

Cubical/Relation/Nullary/Base.agda

@@ -24,6 +24,10 @@ data Dec (P : Type ℓ) : Type ℓ where
   yes : ( p :   P) → Dec P
   no  : (¬p : ¬ P) → Dec P
 
+decRec : ∀ {ℓ ℓ'} {P : Type ℓ} {A : Type ℓ'} → (P → A) → (¬ P → A) → (Dec P) → A
+decRec ifyes ifno (yes p) = ifyes p
+decRec ifyes ifno (no ¬p) = ifno ¬p
+
 NonEmpty : Type ℓ → Type ℓ
 NonEmpty A = ¬ ¬ A