{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Fixpoint
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma.Base using (_×_)
open import Cubical.Data.Sum.Base
open import Cubical.Relation.Nullary.Base
open import Cubical.HITs.PropositionalTruncation.Base
private
variable
ℓ ℓ' : Level
A B : Type ℓ
P : A -> Type ℓ
sectionDiscrete
: (f : A → B) (g : B → A) → section f g → Discrete A → Discrete B
sectionDiscrete f g sect dA x y with dA (g x) (g y)
... | yes p = yes (sym (sect x) ∙∙ cong f p ∙∙ sect y)
... | no ¬p = no (λ p → ¬p (cong g p))
isoPresDiscrete : Iso A B → Discrete A → Discrete B
isoPresDiscrete e = sectionDiscrete fun inv rightInv
where open Iso e
EquivPresDiscrete : ∀ {ℓ ℓ'}{A : Type ℓ} {B : Type ℓ'} → A ≃ B
→ Discrete A → Discrete B
EquivPresDiscrete e = isoPresDiscrete (equivToIso e)
isProp¬ : (A : Type ℓ) → isProp (¬ A)
isProp¬ A p q i x = isProp⊥ (p x) (q x) i
Stable¬ : Stable (¬ A)
Stable¬ ¬¬¬a a = ¬¬¬a ¬¬a
where
¬¬a = λ ¬a → ¬a a
StableΠ : (∀ x → Stable (P x)) -> Stable (∀ x → P x)
StableΠ Ps e x = Ps x λ k → e λ f → k (f x)
Stable→ : Stable B → Stable (A → B)
Stable→ Bs = StableΠ (λ _ → Bs)
Stable× : Stable A -> Stable B -> Stable (A × B)
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
discreteDec : (Adis : Discrete A) → Discrete (Dec A)
discreteDec Adis (yes p) (yes p') = decideYes (Adis p p')
where
decideYes : Dec (p ≡ p') → Dec (yes p ≡ yes p')
decideYes (yes eq) = yes (cong yes eq)
decideYes (no ¬eq) = no λ eq → ¬eq (cong (fromYes p) eq)
discreteDec Adis (yes p) (no ¬p) = ⊥.rec (¬p p)
discreteDec Adis (no ¬p) (yes p) = ⊥.rec (¬p p)
discreteDec {A = A} Adis (no ¬p) (no ¬p') = yes (cong no (isProp¬ A ¬p ¬p'))
isPropDec : (Aprop : isProp A) → isProp (Dec A)
isPropDec Aprop (yes a) (yes a') = cong yes (Aprop a a')
isPropDec Aprop (yes a) (no ¬a) = ⊥.rec (¬a a)
isPropDec Aprop (no ¬a) (yes a) = ⊥.rec (¬a a)
isPropDec {A = A} Aprop (no ¬a) (no ¬a') = cong no (isProp¬ A ¬a ¬a')
mapDec : ∀ {B : Type ℓ} → (A → B) → (¬ A → ¬ B) → Dec A → Dec B
mapDec f _ (yes p) = yes (f p)
mapDec _ f (no ¬p) = no (f ¬p)
EquivPresDec : ∀ {ℓ ℓ'}{A : Type ℓ} {B : Type ℓ'} → A ≃ B
→ Dec A → Dec B
EquivPresDec p = mapDec (p .fst) (λ f → f ∘ invEq p)
¬→¬∥∥ : ¬ A → ¬ ∥ A ∥₁
¬→¬∥∥ ¬p ∣ a ∣₁ = ¬p a
¬→¬∥∥ ¬p (squash₁ x y i) = isProp⊥ (¬→¬∥∥ ¬p x) (¬→¬∥∥ ¬p y) i
Dec∥∥ : Dec A → Dec ∥ A ∥₁
Dec∥∥ = mapDec ∣_∣₁ ¬→¬∥∥
open Cubical.HITs.PropositionalTruncation.Base
populatedBy : ∥ A ∥₁ → ⟪ A ⟫
populatedBy {A = A} a (f , fIsConst) = h a where
h : ∥ A ∥₁ → Fixpoint f
h ∣ a ∣₁ = f a , fIsConst (f a) a
h (squash₁ a b i) = 2-Constant→isPropFixpoint f fIsConst (h a) (h b) i
notEmptyPopulated : ⟪ A ⟫ → NonEmpty A
notEmptyPopulated {A = A} pop u = u (fixpoint (pop (h , hIsConst))) where
h : A → A
h a = ⊥.elim (u a)
hIsConst : ∀ x y → h x ≡ h y
hIsConst x y i = ⊥.elim (isProp⊥ (u x) (u y) i)
Dec→Stable : Dec A → Stable A
Dec→Stable (yes x) = λ _ → x
Dec→Stable (no x) = λ f → ⊥.elim (f x)
Stable→PStable : Stable A → PStable A
Stable→PStable st = st ∘ notEmptyPopulated
PStable→SplitSupport : PStable A → SplitSupport A
PStable→SplitSupport pst = pst ∘ populatedBy
SplitSupport→Collapsible : SplitSupport A → Collapsible A
SplitSupport→Collapsible {A = A} hst = h , hIsConst where
h : A → A
h p = hst ∣ p ∣₁
hIsConst : 2-Constant h
hIsConst p q i = hst (squash₁ ∣ p ∣₁ ∣ q ∣₁ i)
Collapsible→SplitSupport : Collapsible A → SplitSupport A
Collapsible→SplitSupport f x = fixpoint (populatedBy x f)
HSeparated→Collapsible≡ : HSeparated A → Collapsible≡ A
HSeparated→Collapsible≡ hst x y = SplitSupport→Collapsible (hst x y)
Collapsible≡→HSeparated : Collapsible≡ A → HSeparated A
Collapsible≡→HSeparated col x y = Collapsible→SplitSupport (col x y)
Collapsible≡→isSet : Collapsible≡ A → isSet A
Collapsible≡→isSet {A = A} col a b p q = p≡q where
f : (x : A) → a ≡ x → a ≡ x
f x = col a x .fst
fIsConst : (x : A) → (p q : a ≡ x) → f x p ≡ f x q
fIsConst x = col a x .snd
rem : (p : a ≡ b) → PathP (λ i → a ≡ p i) (f a refl) (f b p)
rem p j = f (p j) (λ i → p (i ∧ j))
p≡q : p ≡ q
p≡q j i = hcomp (λ k → λ { (i = i0) → f a refl k
; (i = i1) → fIsConst b p q j k
; (j = i0) → rem p i k
; (j = i1) → rem q i k }) a
HSeparated→isSet : HSeparated A → isSet A
HSeparated→isSet = Collapsible≡→isSet ∘ HSeparated→Collapsible≡
isSet→HSeparated : isSet A → HSeparated A
isSet→HSeparated setA x y = extract where
extract : ∥ x ≡ y ∥₁ → x ≡ y
extract ∣ p ∣₁ = p
extract (squash₁ p q i) = setA x y (extract p) (extract q) i
PStable≡→HSeparated : PStable≡ A → HSeparated A
PStable≡→HSeparated pst x y = PStable→SplitSupport (pst x y)
PStable≡→isSet : PStable≡ A → isSet A
PStable≡→isSet = HSeparated→isSet ∘ PStable≡→HSeparated
Separated→PStable≡ : Separated A → PStable≡ A
Separated→PStable≡ st x y = Stable→PStable (st x y)
Separated→isSet : Separated A → isSet A
Separated→isSet = PStable≡→isSet ∘ Separated→PStable≡
SeparatedΠ : (∀ x → Separated (P x)) -> Separated ((x : A) -> P x)
SeparatedΠ Ps f g e i x = Ps x (f x) (g x) (λ k → e (k ∘ cong (λ f → f x))) i
Separated→ : Separated B -> Separated (A → B)
Separated→ Bs = SeparatedΠ (λ _ → Bs)
Separated× : Separated A -> Separated B -> Separated (A × B)
Separated× As Bs p q e i = λ where
.fst → As (fst p) (fst q) (λ k → e λ r → k (cong fst r)) i
.snd → Bs (snd p) (snd q) (λ k → e λ r → k (cong snd r)) i
Discrete→Separated : Discrete A → Separated A
Discrete→Separated d x y = Dec→Stable (d x y)
Discrete→isSet : Discrete A → isSet A
Discrete→isSet = Separated→isSet ∘ Discrete→Separated
≡no : ∀ {A : Type ℓ} x y → Path (Dec A) x (no y)
≡no (yes p) y = ⊥.rec (y p)
≡no (no ¬p) y i = no (isProp¬ _ ¬p y i)
inhabitedFibres? : ∀ {ℓ'} {A : Type ℓ} {B : Type ℓ'}
(f : A → B) → Type (ℓ-max ℓ ℓ')
inhabitedFibres? {A = A} {B = B} f =
(y : B) → (Σ[ x ∈ A ] f x ≡ y) ⊎ ((x : A) → ¬ f x ≡ y)