{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.HITs.PropositionalTruncation as ∥∥
open import Cubical.HITs.SetTruncation as ∥∥₀
open import Cubical.HITs.SetQuotients as []
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
toSingl : {ℓ : Level} {A : Type ℓ} (a : A) → singl a
toSingl a = a , refl
cong₂-nd : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
(f : A → B → C)
{x y : A} (p : x ≡ y)
{u v : B} (q : u ≡ v) →
f x u ≡ f y v
cong₂-nd f p q = cong₂ f p q
cong₃-nd : {ℓ ℓ' ℓ'' ℓ''' : Level} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
(f : A → B → C → D)
{x y : A} (p : x ≡ y)
{u v : B} (q : u ≡ v)
{s t : C} (r : s ≡ t)→
f x u s ≡ f y v t
cong₃-nd f p q r i = f (p i) (q i) (r i)
subst₂ : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} (C : A → B → Type ℓ'') {a a' : A} (p : a ≡ a') {b b' : B} (q : b ≡ b') → C a b → C a' b'
subst₂ B {a' = a'} p {b = b} q x = subst (B a') q (subst (λ a → B a b) p x)
postulate
funExtP : {ℓ ℓ' : Level} {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
{f : (a : A i0) → B i0 a} {g : (a : A i1) → B i1 a} →
({x : A i0} {y : A i1} (p : PathP A x y) → PathP (λ i → B i (p i)) (f x) (g y)) →
PathP (λ i → (a : A i) → B i a) f g
isPropΠ' : {ℓ ℓ' : Level} {A : Type ℓ} {B : A → Type ℓ'} → (h : (x : A) → isProp (B x)) → isProp ({x : A} → B x)
isPropΠ' h f g i {x} = h x (f {x}) (g {x}) i
isPropΣ' : {ℓ ℓ' : Level} {A : Type ℓ} {B : A → Type ℓ'} → ((x : A) → isProp (B x)) → ((x y : A) → B x → B y → x ≡ y) → isProp (Σ A B)
isPropΣ' prop eq (a , b) (a' , b') = ΣPathP ((eq _ _ b b') , (toPathP (prop _ _ _)))
∥∥-elim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (SB : isSet B) (f : A → B) → ((a a' : A) → f a ≡ f a') → ∥ A ∥₁ → B
∥∥-elim {ℓ} {ℓ'} {A} {B} SB f p a = fst (F a)
where
im : Type (ℓ-max ℓ ℓ')
im = Σ B (λ b → ∥ Σ A (λ a → f a ≡ b) ∥₁)
im-isProp : isProp im
im-isProp (b , e) (b' , e') = ΣPathP (b≡b' , toPathP (isPropPropTrunc _ e'))
where
b≡b' : b ≡ b'
b≡b' = ∥∥.elim (λ _ → SB b b') (λ { (a , q) → ∥∥.elim (λ _ → SB b b') (λ { (a' , q') → sym q ∙ p a a' ∙ q' }) e' }) e
F : ∥ A ∥₁ → im
F a = ∥∥.elim (λ _ → im-isProp) (λ a → f a , ∣ a , refl ∣₁) a
Π≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {B C : A → Type ℓ'} → ((x : A) → B x ≡ C x) → ((x : A) → B x) ≡ ((x : A) → C x)
Π≡ {A = A} p i = (x : A) → p x i
Σfun : {ℓ ℓ' : Level} {A A' : Type ℓ} {B : A → Type ℓ'} {B' : A' → Type ℓ'} →
(f : A → A') (g : {a : A} → B a → B' (f a)) →
(Σ A B → Σ A' B')
Σfun f g (a , b) = (f a , g b)
equivΣProp : {ℓ ℓ' : Level} {A A' : Type ℓ} {B : A → Type ℓ'} {B' : A' → Type ℓ'}
(e : A ≃ A')
(g : {a : A} → B a → B' (equivFun e a)) (g' : {a' : A'} → B' a' → B (invEq e a')) → ((a : A) → isProp (B a)) → ((a' : A') → isProp (B' a')) →
Σ A B ≃ Σ A' B'
equivΣProp {_} {_} {A} {A'} {B} {B'} e g g' P P' = isoToEquiv i
where
f : A → A'
f = equivFun e
fi : Iso A A'
fi = equivToIso e
i : Iso (Σ A B) (Σ A' B')
Iso.fun i = Σfun f g
Iso.inv i = Σfun (Iso.inv fi) g'
Iso.rightInv i (a' , b') = Σ≡Prop P' (Iso.rightInv fi a')
Iso.leftInv i (a , b) = Σ≡Prop P (Iso.leftInv fi a)
⊎-×-≃ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
⊎-×-≃ {A = A} {B = B} {C = C} = isoToEquiv (iso f g f-g g-f)
where
f : (A ⊎ B) × C → (A × C) ⊎ (B × C)
f (inl a , c) = inl (a , c)
f (inr b , c) = inr (b , c)
g : (A × C) ⊎ (B × C) → (A ⊎ B) × C
g (inl (a , c)) = (inl a) , c
g (inr (b , c)) = (inr b) , c
g-f : (x : (A ⊎ B) × C) → g (f x) ≡ x
g-f (inl a , c) = refl
g-f (inr b , c) = refl
f-g : (x : (A × C) ⊎ (B × C)) → f (g x) ≡ x
f-g (inl (a , c)) = refl
f-g (inr (b , c)) = refl
Σ-ap :
∀ {ℓ ℓ'} {X X' : Type ℓ} {Y : X → Type ℓ'} {Y' : X' → Type ℓ'}
→ (isom : X ≡ X')
→ ((x : X) → Y x ≡ Y' (transport isom x))
→ (Σ X Y) ≡ (Σ X' Y')
Σ-ap {X = X} p q = ua (Σ-cong-equiv (pathToEquiv p) (λ x → pathToEquiv (q x)))
isInjection : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → (A → B) → Type (ℓ-max ℓ ℓ')
isInjection {A = A} f = {x y : A} → f x ≡ f y → x ≡ y
isEmbedding→isInjection : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} {f : A → B} → isEmbedding f → isInjection f
isEmbedding→isInjection emb = invEq (_ , emb _ _)
private
variable
ℓ ℓ' : Level
A : Type ℓ
B : Type ℓ'
disjoint-coprod' : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {a : A} {b : B} → inl a ≡ inr b → Lift {_} {ℓ} ⊥
disjoint-coprod' {ℓ} {ℓ'} {A = A} {B = B} {a} p = subst A⊥ p a
where
A⊥ : A ⊎ B → Type ℓ
A⊥ (inl _) = A
A⊥ (inr _) = Lift ⊥
disjoint-coprod : {a : A} {b : B} → inl a ≡ inr b → ⊥
disjoint-coprod p with disjoint-coprod' p
... | ()
inl≢inr = disjoint-coprod
inl-injective : {x y : A} → inl {B = B} x ≡ inl y → x ≡ y
inl-injective p = isEmbedding→isInjection isEmbedding-inl p
inr-injective : {x y : B} → inr {A = A} x ≡ inr y → x ≡ y
inr-injective p = isEmbedding→isInjection isEmbedding-inr p
coprod-case : (x : A ⊎ B) → Σ A (λ a → x ≡ inl a) ⊎ Σ B (λ b → x ≡ inr b)
coprod-case (inl a) = inl (a , refl)
coprod-case (inr b) = inr (b , refl)
data in-left {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} : A ⊎ B → Type (ℓ-max ℓ ℓ') where
is-inl : (a : A) → in-left (inl a)
data in-right {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} : A ⊎ B → Type (ℓ-max ℓ ℓ') where
is-inr : (b : B) → in-right (inr b)
in-left-isProp : (x : A ⊎ B) → isProp (in-left x)
in-left-isProp .(inl a) (is-inl a) (is-inl .a) = refl
in-right-isProp : (x : A ⊎ B) → isProp (in-right x)
in-right-isProp .(inr b) (is-inr b) (is-inr .b) = refl
is-left : {x : A ⊎ B} → in-left x → Σ A (λ a → x ≡ inl a)
is-left (is-inl a) = a , refl
is-right : {x : A ⊎ B} → in-right x → Σ B (λ b → x ≡ inr b)
is-right (is-inr b) = b , refl
get-left : {x : A ⊎ B} → in-left x → A
get-left (is-inl a) = a
get-right : {x : A ⊎ B} → in-right x → B
get-right (is-inr b) = b
inl-get-left : {x : A ⊎ B} (l : in-left x) → inl (get-left l) ≡ x
inl-get-left (is-inl a) = refl
inr-get-right : {x : A ⊎ B} (r : in-right x) → inr (get-right r) ≡ x
inr-get-right (is-inr b) = refl
inl≃ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ Σ (A ⊎ B) in-left
inl≃ = isoToEquiv i
where
i : Iso A (Σ (A ⊎ B) in-left)
Iso.fun i a = inl a , is-inl a
Iso.inv i (_ , l) = get-left l
Iso.rightInv i (_ , l) = Σ≡Prop in-left-isProp (inl-get-left l)
Iso.leftInv i a = refl
inr≃ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → B ≃ Σ (A ⊎ B) in-right
inr≃ = isoToEquiv i
where
i : Iso B (Σ (A ⊎ B) in-right)
Iso.fun i b = inr b , is-inr b
Iso.inv i (_ , r) = get-right r
Iso.rightInv i (_ , r) = Σ≡Prop in-right-isProp (inr-get-right r)
Iso.leftInv i b = refl
Discrete⊎ : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → Discrete A → Discrete B → Discrete (A ⊎ B)
Discrete⊎ DA DB (inl x) (inl y) with DA x y
... | yes p = yes (cong inl p)
... | no ¬p = no (¬p ∘ inl-injective)
Discrete⊎ DA DB (inr x) (inr y) with DB x y
... | yes p = yes (cong inr p)
... | no ¬p = no (¬p ∘ inr-injective)
Discrete⊎ DA DB (inl x) (inr y) = no inl≢inr
Discrete⊎ DA DB (inr x) (inl y) = no (inl≢inr ∘ sym)
Discrete× : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → Discrete A → Discrete B → Discrete (A × B)
Discrete× DA DB (a , b) (a' , b') with DA a a' | DB b b'
... | yes p | yes q = yes (ΣPathP (p , q))
... | yes p | no ¬q = no (¬q ∘ cong snd)
... | no ¬p | _ = no (¬p ∘ cong fst)
Dec× : {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} → Dec A → Dec B → Dec (A × B)
Dec× (yes a) (yes b) = yes (a , b)
Dec× (yes a) (no ¬b) = no λ { (_ , b) → ¬b b}
Dec× (no ¬a) (yes b) = no λ { (a , _) → ¬a a}
Dec× (no ¬a) (no ¬b) = no λ { (a , b) → ¬a a}
Dec¬ : {ℓ : Level} {A : Type ℓ} → Dec A → Dec (¬ A)
Dec¬ (yes a) = no λ ¬a → ¬a a
Dec¬ (no ¬a) = yes λ a → ¬a a
Dec→NNE : {ℓ : Level} {A : Type ℓ} → Dec A → ¬ ¬ A → A
Dec→NNE (yes a) ¬¬a = a
Dec→NNE (no ¬a) ¬¬a = ⊥.elim (¬¬a ¬a)
¬∀¬¬⇒¬¬∃¬ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ¬ ((x : A) → ¬ ¬ (B x)) → ¬ ¬ (Σ A (λ x → ¬ (B x)))
¬∀¬¬⇒¬¬∃¬ f g = f λ a b → g (a , b)