{-# OPTIONS --without-K #-}
open import Equality
module Univalence-axiom
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open import Bijection eq as Bijection using (_↔_)
open import Bool eq
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq
hiding (id; inverse) renaming (_∘_ to _⊚_)
open import Function-universe eq as F hiding (id; _∘_)
open import Groupoid eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Injection eq using (Injective)
open import Logical-equivalence hiding (id; _∘_; inverse)
import Nat eq as Nat
open import Prelude
open import Surjection eq hiding (id; _∘_; ∃-cong)
≡⇒≃ : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A ≃ B
≡⇒≃ = ≡⇒↝ equivalence
Univalence′ : ∀ {ℓ} → Set ℓ → Set ℓ → Set (lsuc ℓ)
Univalence′ A B = Is-equivalence (≡⇒≃ {A = A} {B = B})
Univalence : ∀ ℓ → Set (lsuc ℓ)
Univalence ℓ = {A B : Set ℓ} → Univalence′ A B
≡≃≃ : ∀ {ℓ} {A B : Set ℓ} → Univalence′ A B → (A ≡ B) ≃ (A ≃ B)
≡≃≃ univ = ⟨ ≡⇒≃ , univ ⟩
≡≃↔ : ∀ {ℓ} {A B : Set ℓ} →
Univalence′ A B →
Extensionality ℓ ℓ →
Is-set A →
(A ≡ B) ≃ (A ↔ B)
≡≃↔ {A = A} {B} univ ext A-set =
(A ≡ B) ↝⟨ ≡≃≃ univ ⟩
(A ≃ B) ↔⟨ inverse $ ↔↔≃ ext A-set ⟩□
(A ↔ B) □
≡⇒→ : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
≡⇒→ = _≃_.to ∘ ≡⇒≃
≡⇒← : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → B → A
≡⇒← = _≃_.from ∘ ≡⇒≃
≃⇒≡ : ∀ {ℓ} {A B : Set ℓ} → Univalence′ A B → A ≃ B → A ≡ B
≃⇒≡ univ = _≃_.from (≡≃≃ univ)
Propositional-extensionality : (ℓ : Level) → Set (lsuc ℓ)
Propositional-extensionality ℓ =
{A B : Set ℓ} → Is-proposition A → Is-proposition B → A ⇔ B → A ≡ B
Propositional-extensionality-is-univalence-for-propositions :
∀ {ℓ} →
Extensionality (lsuc ℓ) (lsuc ℓ) →
Propositional-extensionality ℓ
≃
({A B : Set ℓ} →
Is-proposition A → Is-proposition B → Univalence′ A B)
Propositional-extensionality-is-univalence-for-propositions {ℓ} ext =
_↔_.to (⇔↔≃ ext
([inhabited⇒+]⇒+ 0 λ prop-ext →
implicit-Π-closure ext 1 λ _ →
implicit-Π-closure ext 1 λ _ →
Π-closure (lower-extensionality _ lzero ext) 1 λ A-prop →
Π-closure (lower-extensionality _ lzero ext) 1 λ B-prop →
Π-closure (lower-extensionality _ lzero ext) 1 λ _ →
≡-closure (prop-ext {_}) A-prop B-prop)
(implicit-Π-closure ext 1 λ _ →
implicit-Π-closure ext 1 λ _ →
Π-closure (lower-extensionality _ lzero ext) 1 λ _ →
Π-closure (lower-extensionality _ lzero ext) 1 λ _ →
Eq.propositional ext _))
(record
{ to = λ prop-ext A-prop B-prop A≃B →
( prop-ext A-prop B-prop (_≃_.logical-equivalence A≃B)
, _⇔_.to propositional⇔irrelevant
(Eq.left-closure (lower-extensionality _ _ ext)
0 A-prop)
_ _
) , λ _ → Σ-≡,≡→≡
(_⇔_.to propositional⇔irrelevant
(≡-closure prop-ext A-prop B-prop)
_ _)
(_⇔_.to propositional⇔irrelevant
(mono₁ 1 (Eq.left-closure
(lower-extensionality _ _ ext)
0 A-prop)
_ _)
_ _)
; from = λ univ {A B} A-prop B-prop →
A ⇔ B ↔⟨ ⇔↔≃ (lower-extensionality _ _ ext) A-prop B-prop ⟩
A ≃ B ↔⟨ inverse ⟨ _ , univ A-prop B-prop ⟩ ⟩□
A ≡ B □
})
where
⇔≃≡ :
Propositional-extensionality ℓ →
{A B : Set ℓ} →
Is-proposition A → Is-proposition B →
(A ⇔ B) ≃ (A ≡ B)
⇔≃≡ prop-ext {A} {B} A-prop B-prop =
A ⇔ B ↝⟨ proj₂ (propositional-identity≃≡
(λ (A B : Proposition ℓ) → proj₁ A ⇔ proj₁ B)
(λ { (A , A-prop) (B , B-prop) →
⇔-closure (lower-extensionality _ _ ext)
1 A-prop B-prop })
(λ _ → F.id)
(λ { (A , A-prop) (B , B-prop) A⇔B →
Σ-≡,≡→≡ (prop-ext A-prop B-prop A⇔B)
(_⇔_.to propositional⇔irrelevant
(H-level-propositional
(lower-extensionality _ _ ext) 1)
_ _) }))
ext ⟩
(A , A-prop) ≡ (B , B-prop) ↔⟨ inverse $ ignore-propositional-component
(H-level-propositional
(lower-extensionality _ _ ext) 1) ⟩□
A ≡ B □
≡-closure :
Propositional-extensionality ℓ →
{A B : Set ℓ} →
Is-proposition A → Is-proposition B → Is-proposition (A ≡ B)
≡-closure prop-ext A-prop B-prop =
H-level.respects-surjection
(_≃_.surjection (⇔≃≡ prop-ext A-prop B-prop))
1
(⇔-closure (lower-extensionality _ _ ext) 1 A-prop B-prop)
abstract
≡⇒≃-refl : ∀ {a} {A : Set a} →
≡⇒≃ (refl A) ≡ Eq.id
≡⇒≃-refl = ≡⇒↝-refl
≡⇒→-refl : ∀ {a} {A : Set a} →
≡⇒→ (refl A) ≡ id
≡⇒→-refl = cong _≃_.to ≡⇒≃-refl
≡⇒←-refl : ∀ {a} {A : Set a} →
≡⇒← (refl A) ≡ id
≡⇒←-refl = cong _≃_.from ≡⇒≃-refl
≃⇒≡-id : ∀ {a} {A : Set a}
(univ : Univalence′ A A) →
≃⇒≡ univ Eq.id ≡ refl A
≃⇒≡-id univ =
≃⇒≡ univ Eq.id ≡⟨ sym $ cong (≃⇒≡ univ) ≡⇒≃-refl ⟩
≃⇒≡ univ (≡⇒≃ (refl _)) ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
refl _ ∎
≡⇒→-≃⇒≡ : ∀ k {ℓ} {A B : Set ℓ} {eq : A ≃ B}
(univ : Univalence′ A B) →
to-implication (≡⇒↝ k (≃⇒≡ univ eq)) ≡ _≃_.to eq
≡⇒→-≃⇒≡ k {eq = eq} univ =
to-implication (≡⇒↝ k (≃⇒≡ univ eq)) ≡⟨ to-implication-≡⇒↝ k _ ⟩
≡⇒↝ implication (≃⇒≡ univ eq) ≡⟨ sym $ to-implication-≡⇒↝ equivalence _ ⟩
≡⇒→ (≃⇒≡ univ eq) ≡⟨ cong _≃_.to (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩∎
_≃_.to eq ∎
module _ (univ : Univalence′ Bool Bool) where
swap-as-an-equality : Bool ≡ Bool
swap-as-an-equality = ≃⇒≡ univ (Eq.↔⇒≃ swap)
abstract
swap≢refl : swap-as-an-equality ≢ refl Bool
swap≢refl =
swap-as-an-equality ≡ refl _ ↝⟨ cong ≡⇒→ ⟩
≡⇒→ swap-as-an-equality ≡ ≡⇒→ (refl _) ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) ⟩
not ≡ id ↝⟨ cong (_$ false) ⟩
true ≡ false ↝⟨ Bool.true≢false ⟩□
⊥ □
¬-Set-set : ¬ Is-set Set
¬-Set-set =
Is-set Set ↝⟨ _⇔_.to set⇔UIP ⟩
Uniqueness-of-identity-proofs Set ↝⟨ (λ uip → uip _ _) ⟩
swap-as-an-equality ≡ refl Bool ↝⟨ swap≢refl ⟩□
⊥ □
abstract
¬-Set-set-↑ : ∀ {ℓ} →
Univalence′ (↑ ℓ Bool) (↑ ℓ Bool) →
¬ Is-set (Set ℓ)
¬-Set-set-↑ {ℓ} univ =
Is-set (Set ℓ) ↝⟨ _⇔_.to set⇔UIP ⟩
Uniqueness-of-identity-proofs (Set ℓ) ↝⟨ (λ uip → uip _ _) ⟩
swap-as-an-equality-↑ ≡ refl (↑ ℓ Bool) ↝⟨ swap-↑≢refl ⟩□
⊥ □
where
swap-as-an-equality-↑ : ↑ ℓ Bool ≡ ↑ ℓ Bool
swap-as-an-equality-↑ =
≃⇒≡ univ $
Eq.↔⇒≃ $
(Bijection.inverse Bijection.↑↔
Bijection.∘
swap
Bijection.∘
Bijection.↑↔)
swap-↑≢refl : swap-as-an-equality-↑ ≢ refl (↑ ℓ Bool)
swap-↑≢refl =
swap-as-an-equality-↑ ≡ refl _ ↝⟨ cong ≡⇒→ ⟩
≡⇒→ swap-as-an-equality-↑ ≡ ≡⇒→ (refl _) ↝⟨ subst (uncurry _≡_) (cong₂ _,_ (≡⇒→-≃⇒≡ equivalence univ) ≡⇒→-refl) ⟩
lift ∘ not ∘ lower ≡ id ↝⟨ cong (lower ∘ (_$ lift false)) ⟩
true ≡ false ↝⟨ Bool.true≢false ⟩□
⊥ □
abstract
equality-can-have-infinitely-many-inhabitants :
Univalence′ ℕ ℕ →
∃ λ (A : Set) → ∃ λ (B : Set) →
∃ λ (p : ℕ → A ≡ B) → Injective p
equality-can-have-infinitely-many-inhabitants univ =
(ℕ , ℕ , cast ∘ p , cast-preserves-injections p p-injective)
where
cast : ℕ ≃ ℕ → ℕ ≡ ℕ
cast = ≃⇒≡ univ
cast-preserves-injections :
{A : Set} (f : A → ℕ ≃ ℕ) →
Injective f → Injective (cast ∘ f)
cast-preserves-injections f inj {x = x} {y = y} cast-f-x≡cast-f-y =
inj (f x ≡⟨ sym $ _≃_.right-inverse-of (≡≃≃ univ) (f x) ⟩
≡⇒≃ (cast (f x)) ≡⟨ cong ≡⇒≃ cast-f-x≡cast-f-y ⟩
≡⇒≃ (cast (f y)) ≡⟨ _≃_.right-inverse-of (≡≃≃ univ) (f y) ⟩∎
f y ∎)
swap_and-0 : ℕ → ℕ → ℕ
swap i and-0 zero = i
swap i and-0 (suc n) with i Nat.≟ suc n
... | yes i≡1+n = zero
... | no i≢1+n = suc n
swap∘swap : ∀ i n → swap i and-0 (swap i and-0 n) ≡ n
swap∘swap zero zero = refl zero
swap∘swap (suc i) zero with i Nat.≟ i
... | yes _ = refl 0
... | no i≢i = ⊥-elim $ i≢i (refl i)
swap∘swap i (suc n) with i Nat.≟ suc n
... | yes i≡1+n = i≡1+n
... | no i≢1+n with i Nat.≟ suc n
... | yes i≡1+n = ⊥-elim $ i≢1+n i≡1+n
... | no _ = refl (suc n)
p : ℕ → ℕ ≃ ℕ
p i = ↔⇒≃ record
{ surjection = record
{ logical-equivalence = record { to = swap i and-0
; from = swap i and-0
}
; right-inverse-of = swap∘swap i
}
; left-inverse-of = swap∘swap i
}
p-injective : Injective p
p-injective {x = i₁} {y = i₂} p-i₁≡p-i₂ =
i₁ ≡⟨ refl i₁ ⟩
swap i₁ and-0 0 ≡⟨ cong (λ f → f 0) swap-i₁≡swap-i₂ ⟩
swap i₂ and-0 0 ≡⟨ refl i₂ ⟩∎
i₂ ∎
where
swap-i₁≡swap-i₂ : swap i₁ and-0 ≡ swap i₂ and-0
swap-i₁≡swap-i₂ = cong _≃_.to p-i₁≡p-i₂
abstract
transport-theorem :
∀ {p₁ p₂} (P : Set p₁ → Set p₂) →
(resp : ∀ {A B} → A ≃ B → P A → P B) →
(∀ {A} (p : P A) → resp Eq.id p ≡ p) →
∀ {A B} (univ : Univalence′ A B) →
(A≃B : A ≃ B) (p : P A) →
resp A≃B p ≡ subst P (≃⇒≡ univ A≃B) p
transport-theorem P resp resp-id univ A≃B p =
resp A≃B p ≡⟨ sym $ cong (λ q → resp q p) (right-inverse-of A≃B) ⟩
resp (to (from A≃B)) p ≡⟨ elim (λ {A B} A≡B → ∀ p →
resp (≡⇒≃ A≡B) p ≡ subst P A≡B p)
(λ A p →
resp (≡⇒≃ (refl A)) p ≡⟨ trans (cong (λ q → resp q p) ≡⇒↝-refl) (resp-id p) ⟩
p ≡⟨ sym $ subst-refl P p ⟩∎
subst P (refl A) p ∎) _ _ ⟩∎
subst P (from A≃B) p ∎
where open _≃_ (≡≃≃ univ)
resp-is-equivalence :
∀ {p₁ p₂} (P : Set p₁ → Set p₂) →
(resp : ∀ {A B} → A ≃ B → P A → P B) →
(∀ {A} (p : P A) → resp Eq.id p ≡ p) →
∀ {A B} (univ : Univalence′ A B) →
(A≃B : A ≃ B) → Is-equivalence (resp A≃B)
resp-is-equivalence P resp resp-id univ A≃B =
Eq.respects-extensional-equality
(λ p → sym $ transport-theorem P resp resp-id univ A≃B p)
(subst-is-equivalence P (≃⇒≡ univ A≃B))
precomposition-is-equivalence :
∀ {ℓ c} {A B : Set ℓ} {C : Set c} →
Univalence′ B A → (A≃B : A ≃ B) →
Is-equivalence (λ (g : B → C) → g ∘ _≃_.to A≃B)
precomposition-is-equivalence {ℓ} {c} {C = C} univ A≃B =
resp-is-equivalence P resp refl univ (Eq.inverse A≃B)
where
P : Set ℓ → Set (ℓ ⊔ c)
P X = X → C
resp : ∀ {A B} → A ≃ B → P A → P B
resp A≃B p = p ∘ _≃_.from A≃B
precompositions-cancel :
∀ {ℓ c} {A B : Set ℓ} {C : Set c} →
Univalence′ B A → (A≃B : A ≃ B) {f g : B → C} →
let open _≃_ A≃B in
f ∘ to ≡ g ∘ to → f ≡ g
precompositions-cancel univ A≃B {f} {g} f∘to≡g∘to =
f ≡⟨ sym $ left-inverse-of f ⟩
from (to f) ≡⟨ cong from f∘to≡g∘to ⟩
from (to g) ≡⟨ left-inverse-of g ⟩∎
g ∎
where open _≃_ (⟨ _ , precomposition-is-equivalence univ A≃B ⟩)
_²/≡ : ∀ {ℓ} → Set ℓ → Set ℓ
A ²/≡ = ∃ λ (x : A) → ∃ λ (y : A) → y ≡ x
-²/≡↔- : ∀ {a} {A : Set a} → (A ²/≡) ↔ A
-²/≡↔- {A = A} =
(∃ λ (x : A) → ∃ λ (y : A) → y ≡ x) ↝⟨ ∃-cong (λ _ → inverse $ _⇔_.to contractible⇔⊤↔ (singleton-contractible _)) ⟩
A × ⊤ ↝⟨ ×-right-identity ⟩□
A □
abstract
extensionality :
∀ {a b} {A : Set a} {B : Set b} →
Univalence′ (B ²/≡) B →
{f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
extensionality {A = A} {B} univ {f} {g} f≡g =
f ≡⟨ refl f ⟩
f′ ∘ pair ≡⟨ cong (λ (h : B ²/≡ → B) → h ∘ pair) f′≡g′ ⟩
g′ ∘ pair ≡⟨ refl g ⟩∎
g ∎
where
f′ : B ²/≡ → B
f′ = proj₁ ∘ proj₂
g′ : B ²/≡ → B
g′ = proj₁
f′≡g′ : f′ ≡ g′
f′≡g′ = precompositions-cancel
univ
(↔⇒≃ $ Bijection.inverse -²/≡↔-)
(refl id)
pair : A → B ²/≡
pair x = (g x , f x , f≡g x)
Π-closure-contractible :
∀ {b} → Univalence′ (Set b ²/≡) (Set b) →
∀ {a} {A : Set a} {B : A → Set b} →
(∀ x → Univalence′ (↑ b ⊤) (B x)) →
(∀ x → Contractible (B x)) → Contractible ((x : A) → B x)
Π-closure-contractible {b} univ₁ {A = A} {B} univ₂ contr =
subst Contractible A→⊤≡[x:A]→Bx →⊤-contractible
where
const-⊤≡B : const (↑ b ⊤) ≡ B
const-⊤≡B = extensionality univ₁ λ x →
_≃_.from (≡≃≃ (univ₂ x)) $ ↔⇒≃ $
Bijection.contractible-isomorphic
(↑-closure 0 ⊤-contractible) (contr x)
A→⊤≡[x:A]→Bx : (A → ↑ b ⊤) ≡ ((x : A) → B x)
A→⊤≡[x:A]→Bx = cong (λ X → (x : A) → X x) const-⊤≡B
→⊤-contractible : Contractible (A → ↑ b ⊤)
→⊤-contractible = (_ , λ _ → refl _)
dependent-extensionality :
∀ {b} → Univalence′ (Set b ²/≡) (Set b) →
∀ {a} {A : Set a} →
(∀ {B : A → Set b} x → Univalence′ (↑ b ⊤) (B x)) →
{B : A → Set b} → Extensionality′ A B
dependent-extensionality univ₁ univ₂ =
_⇔_.to Π-closure-contractible⇔extensionality
(Π-closure-contractible univ₁ univ₂)
Pow : ∀ ℓ {a} → Set a → Set (lsuc (a ⊔ ℓ))
Pow ℓ {a} A = A → Set (a ⊔ ℓ)
Fam : ∀ ℓ {a} → Set a → Set (lsuc (a ⊔ ℓ))
Fam ℓ {a} A = ∃ λ (I : Set (a ⊔ ℓ)) → I → A
Pow⇔Fam : ∀ ℓ {a} {A : Set a} →
Pow ℓ A ⇔ Fam ℓ A
Pow⇔Fam _ = record
{ to = λ P → ∃ P , proj₁
; from = λ { (I , f) a → ∃ λ i → f i ≡ a }
}
Pow↔Fam : ∀ ℓ {a} {A : Set a} →
Extensionality a (lsuc (a ⊔ ℓ)) →
Univalence (a ⊔ ℓ) →
Pow ℓ A ↔ Fam ℓ A
Pow↔Fam ℓ {A = A} ext univ = record
{ surjection = record
{ logical-equivalence = Pow⇔Fam ℓ
; right-inverse-of = λ { (I , f) →
let lemma₁ =
(∃ λ a → ∃ λ i → f i ≡ a) ↔⟨ ∃-comm ⟩
(∃ λ i → ∃ λ a → f i ≡ a) ↔⟨ ∃-cong (λ _ → inverse $ _⇔_.to contractible⇔⊤↔ (other-singleton-contractible _)) ⟩
I × ⊤ ↔⟨ ×-right-identity ⟩□
I □
lemma₂ =
subst (λ I → I → A) (≃⇒≡ univ lemma₁) proj₁ ≡⟨ sym $ transport-theorem (λ I → I → A) (λ eq → _∘ _≃_.from eq) refl univ _ _ ⟩
proj₁ ∘ _≃_.from lemma₁ ≡⟨ refl _ ⟩∎
f ∎
in
(∃ λ a → ∃ λ i → f i ≡ a) , proj₁ ≡⟨ Σ-≡,≡→≡ (≃⇒≡ univ lemma₁) lemma₂ ⟩∎
I , f ∎ }
}
; left-inverse-of = λ P →
let lemma = λ a →
(∃ λ (i : ∃ P) → proj₁ i ≡ a) ↔⟨ inverse Σ-assoc ⟩
(∃ λ a′ → P a′ × a′ ≡ a) ↔⟨ inverse $ ∃-intro _ _ ⟩□
P a □
in
(λ a → ∃ λ (i : ∃ P) → proj₁ i ≡ a) ≡⟨ ext (λ a → ≃⇒≡ univ (lemma a)) ⟩∎
P ∎
}
→↔Σ≃Σ :
∀ ℓ {a b} {A : Set a} {B : Set b} →
Extensionality (a ⊔ b ⊔ ℓ) (lsuc (a ⊔ b ⊔ ℓ)) →
Univalence (a ⊔ b ⊔ ℓ) →
(A → B) ↔ ∃ λ (P : B → Set (a ⊔ b ⊔ ℓ)) → A ≃ Σ B P
→↔Σ≃Σ ℓ {a} {b} {A} {B} ext univ =
(A → B) ↝⟨ →-cong (lower-extensionality lzero _ ext) (inverse Bijection.↑↔) F.id ⟩
(↑ (b ⊔ ℓ) A → B) ↝⟨ inverse ×-left-identity ⟩
⊤ × (↑ _ A → B) ↝⟨ _⇔_.to contractible⇔⊤↔ (singleton-contractible _) ×-cong F.id ⟩
(∃ λ (A′ : Set ℓ′) → A′ ≡ ↑ _ A) × (↑ _ A → B) ↝⟨ inverse Σ-assoc ⟩
(∃ λ (A′ : Set ℓ′) → A′ ≡ ↑ _ A × (↑ _ A → B)) ↝⟨ (∃-cong λ _ → ∃-cong λ eq → →-cong (lower-extensionality lzero _ ext) (≡⇒↝ _ (sym eq)) F.id) ⟩
(∃ λ (A′ : Set ℓ′) → A′ ≡ ↑ _ A × (A′ → B)) ↝⟨ (∃-cong λ _ → ×-comm) ⟩
(∃ λ (A′ : Set ℓ′) → (A′ → B) × A′ ≡ ↑ _ A) ↝⟨ Σ-assoc ⟩
(∃ λ (p : ∃ λ (A′ : Set ℓ′) → A′ → B) → proj₁ p ≡ ↑ _ A) ↝⟨ inverse $ Σ-cong (Pow↔Fam (a ⊔ ℓ) (lower-extensionality ℓ′ lzero ext) univ) (λ _ → F.id) ⟩
(∃ λ (P : B → Set ℓ′) → ∃ P ≡ ↑ _ A) ↔⟨ (∃-cong λ _ → ≡≃≃ univ) ⟩
(∃ λ (P : B → Set ℓ′) → ∃ P ≃ ↑ _ A) ↝⟨ (∃-cong λ _ → Groupoid.⁻¹-bijection (groupoid (lower-extensionality ℓ′ _ ext))) ⟩
(∃ λ (P : B → Set ℓ′) → ↑ _ A ≃ ∃ P) ↔⟨ (∃-cong λ _ → ≃-preserves (lower-extensionality lzero _ ext) (↔⇒≃ Bijection.↑↔) F.id) ⟩□
(∃ λ (P : B → Set ℓ′) → A ≃ ∃ P) □
where
ℓ′ = a ⊔ b ⊔ ℓ
abstract
Univalence′-propositional :
∀ {ℓ} → Extensionality (lsuc ℓ) (lsuc ℓ) →
{A B : Set ℓ} → Is-proposition (Univalence′ A B)
Univalence′-propositional ext =
Eq.propositional ext ≡⇒≃
Univalence-propositional :
∀ {ℓ} → Extensionality (lsuc ℓ) (lsuc ℓ) →
Is-proposition (Univalence ℓ)
Univalence-propositional ext =
implicit-Π-closure ext 1 λ _ →
implicit-Π-closure ext 1 λ _ →
Univalence′-propositional ext
≡⇒≃-sym :
∀ {ℓ} → Extensionality ℓ ℓ →
{A B : Set ℓ} (A≡B : A ≡ B) →
≡⇒≃ (sym A≡B) ≡ Eq.inverse (≡⇒≃ A≡B)
≡⇒≃-sym ext = elim¹
(λ eq → ≡⇒≃ (sym eq) ≡ Eq.inverse (≡⇒≃ eq))
(≡⇒≃ (sym (refl _)) ≡⟨ cong ≡⇒≃ sym-refl ⟩
≡⇒≃ (refl _) ≡⟨ ≡⇒≃-refl ⟩
Eq.id ≡⟨ sym $ Groupoid.identity (Eq.groupoid ext) ⟩
Eq.inverse Eq.id ≡⟨ cong Eq.inverse $ sym ≡⇒≃-refl ⟩∎
Eq.inverse (≡⇒≃ (refl _)) ∎)
≃⇒≡-inverse :
∀ {ℓ} (univ : Univalence ℓ) → Extensionality ℓ ℓ →
{A B : Set ℓ} (A≃B : A ≃ B) →
≃⇒≡ univ (Eq.inverse A≃B) ≡ sym (≃⇒≡ univ A≃B)
≃⇒≡-inverse univ ext A≃B =
≃⇒≡ univ (Eq.inverse A≃B) ≡⟨ sym $ cong (λ p → ≃⇒≡ univ (Eq.inverse p)) (_≃_.right-inverse-of (≡≃≃ univ) _) ⟩
≃⇒≡ univ (Eq.inverse (≡⇒≃ (≃⇒≡ univ A≃B))) ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-sym ext _ ⟩
≃⇒≡ univ (≡⇒≃ (sym (≃⇒≡ univ A≃B))) ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
sym (≃⇒≡ univ A≃B) ∎
≡⇒≃-trans :
∀ {ℓ} → Extensionality ℓ ℓ →
{A B C : Set ℓ} (A≡B : A ≡ B) (B≡C : B ≡ C) →
≡⇒≃ (trans A≡B B≡C) ≡ ≡⇒≃ B≡C ⊚ ≡⇒≃ A≡B
≡⇒≃-trans ext A≡B = elim¹
(λ eq → ≡⇒≃ (trans A≡B eq) ≡ ≡⇒≃ eq ⊚ ≡⇒≃ A≡B)
(≡⇒≃ (trans A≡B (refl _)) ≡⟨ cong ≡⇒≃ $ trans-reflʳ _ ⟩
≡⇒≃ A≡B ≡⟨ sym $ Groupoid.left-identity (Eq.groupoid ext) _ ⟩
Eq.id ⊚ ≡⇒≃ A≡B ≡⟨ sym $ cong (λ eq → eq ⊚ ≡⇒≃ A≡B) ≡⇒≃-refl ⟩∎
≡⇒≃ (refl _) ⊚ ≡⇒≃ A≡B ∎)
≃⇒≡-∘ :
∀ {ℓ} (univ : Univalence ℓ) → Extensionality ℓ ℓ →
{A B C : Set ℓ} (A≃B : A ≃ B) (B≃C : B ≃ C) →
≃⇒≡ univ (B≃C ⊚ A≃B) ≡ trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)
≃⇒≡-∘ univ ext A≃B B≃C =
≃⇒≡ univ (B≃C ⊚ A≃B) ≡⟨ sym $ cong₂ (λ p q → ≃⇒≡ univ (p ⊚ q)) (_≃_.right-inverse-of (≡≃≃ univ) _)
(_≃_.right-inverse-of (≡≃≃ univ) _) ⟩
≃⇒≡ univ (≡⇒≃ (≃⇒≡ univ B≃C) ⊚ ≡⇒≃ (≃⇒≡ univ A≃B)) ≡⟨ cong (≃⇒≡ univ) $ sym $ ≡⇒≃-trans ext _ _ ⟩
≃⇒≡ univ (≡⇒≃ (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C))) ≡⟨ _≃_.left-inverse-of (≡≃≃ univ) _ ⟩∎
trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C) ∎
transport-theorem′ :
∀ {a p r} {A : Set a}
(P : A → Set p) (R : A → A → Set r)
(≡↠R : ∀ {x y} → (x ≡ y) ↠ R x y)
(resp : ∀ {x y} → R x y → P x → P y) →
(∀ x p → resp (_↠_.to ≡↠R (refl x)) p ≡ p) →
∀ {x y} (r : R x y) (p : P x) →
resp r p ≡ subst P (_↠_.from ≡↠R r) p
transport-theorem′ P R ≡↠R resp hyp r p =
resp r p ≡⟨ sym $ cong (λ r → resp r p) (right-inverse-of r) ⟩
resp (to (from r)) p ≡⟨ elim (λ {x y} x≡y → ∀ p →
resp (_↠_.to ≡↠R x≡y) p ≡ subst P x≡y p)
(λ x p →
resp (_↠_.to ≡↠R (refl x)) p ≡⟨ hyp x p ⟩
p ≡⟨ sym $ subst-refl P p ⟩∎
subst P (refl x) p ∎) _ _ ⟩∎
subst P (from r) p ∎
where open _↠_ ≡↠R
transport-theorem′-refl :
∀ {a p r} {A : Set a}
(P : A → Set p) (R : A → A → Set r)
(≡≃R : ∀ {x y} → (x ≡ y) ≃ R x y)
(resp : ∀ {x y} → R x y → P x → P y) →
(resp-refl : ∀ x p → resp (_≃_.to ≡≃R (refl x)) p ≡ p) →
∀ {x} (p : P x) →
transport-theorem′ P R (_≃_.surjection ≡≃R) resp resp-refl
(_≃_.to ≡≃R (refl x)) p ≡
trans (trans (resp-refl x p) (sym $ subst-refl P p))
(sym $ cong (λ eq → subst P eq p)
(_≃_.left-inverse-of ≡≃R (refl x)))
transport-theorem′-refl P R ≡≃R resp resp-refl {x} p =
let body = λ x p → trans (resp-refl x p) (sym $ subst-refl P p)
lemma =
trans (sym $ cong (λ r → resp (to r) p) $ refl (refl x))
(elim (λ {x y} x≡y →
∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
(λ x p → trans (resp-refl x p)
(sym $ subst-refl P p))
(refl x) p) ≡⟨ cong₂ (λ q r → trans q (r p))
(sym $ cong-sym (λ r → resp (to r) p) _)
(elim-refl (λ {x y} x≡y → ∀ p →
resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p) _) ⟩
trans (cong (λ r → resp (to r) p) $ sym $ refl (refl x))
(body x p) ≡⟨ cong (λ q → trans (cong (λ r → resp (to r) p) q) (body x p))
sym-refl ⟩
trans (cong (λ r → resp (to r) p) $ refl (refl x)) (body x p) ≡⟨ cong (λ q → trans q (body x p)) $
cong-refl (λ r → resp (to r) p) ⟩
trans (refl (resp (to (refl x)) p)) (body x p) ≡⟨ trans-reflˡ _ ⟩
body x p ≡⟨ sym $ trans-reflʳ _ ⟩
trans (body x p) (refl (subst P (refl x) p)) ≡⟨ cong (trans (body x p)) $ sym $
cong-refl (λ eq → subst P eq p) ⟩
trans (body x p)
(cong (λ eq → subst P eq p) (refl (refl x))) ≡⟨ cong (trans (body x p) ∘ cong (λ eq → subst P eq p)) $
sym sym-refl ⟩
trans (body x p)
(cong (λ eq → subst P eq p) (sym (refl (refl x)))) ≡⟨ cong (trans (body x p)) $ cong-sym (λ eq → subst P eq p) _ ⟩∎
trans (body x p)
(sym $ cong (λ eq → subst P eq p) (refl (refl x))) ∎
in
trans (sym $ cong (λ r → resp r p) $ right-inverse-of (to (refl x)))
(elim (λ {x y} x≡y →
∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
body (from (to (refl x))) p) ≡⟨ cong (λ eq → trans (sym $ cong (λ r → resp r p) eq)
(elim (λ {x y} x≡y → ∀ p →
resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
body (from (to (refl x))) p)) $
sym $ left-right-lemma (refl x) ⟩
trans (sym $ cong (λ r → resp r p) $ cong to $
left-inverse-of (refl x))
(elim (λ {x y} x≡y →
∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
body (from (to (refl x))) p) ≡⟨ cong (λ eq → trans (sym eq)
(elim (λ {x y} x≡y → ∀ p →
resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
body (from (to (refl x))) p)) $
cong-∘ (λ r → resp r p) to _ ⟩
trans (sym $ cong (λ r → resp (to r) p) $ left-inverse-of (refl x))
(elim (λ {x y} x≡y →
∀ p → resp (_≃_.to ≡≃R x≡y) p ≡ subst P x≡y p)
body (from (to (refl x))) p) ≡⟨ elim₁ (λ {q} eq → trans (sym $ cong (λ r → resp (to r) p) eq)
(elim (λ {x y} x≡y → ∀ p →
resp (_≃_.to ≡≃R x≡y) p ≡
subst P x≡y p)
body q p) ≡
trans (body x p)
(sym $ cong (λ eq → subst P eq p) eq))
lemma
(left-inverse-of (refl x)) ⟩∎
trans (body x p)
(sym $ cong (λ eq → subst P eq p) (left-inverse-of (refl x))) ∎
where open _≃_ ≡≃R
transport-theorem-≡⇒≃-refl :
∀ {p₁ p₂} (P : Set p₁ → Set p₂)
(resp : ∀ {A B} → A ≃ B → P A → P B)
(resp-id : ∀ {A} (p : P A) → resp Eq.id p ≡ p)
(univ : Univalence p₁) {A} (p : P A) →
transport-theorem P resp resp-id univ (≡⇒≃ (refl A)) p ≡
trans (trans (trans (cong (λ eq → resp eq p) ≡⇒≃-refl)
(resp-id p))
(sym $ subst-refl P p))
(sym $ cong (λ eq → subst P eq p)
(_≃_.left-inverse-of (≡≃≃ univ) (refl A)))
transport-theorem-≡⇒≃-refl P resp resp-id univ {A} p =
transport-theorem′-refl P _≃_ (≡≃≃ univ) resp
(λ _ p → trans (cong (λ eq → resp eq p) ≡⇒≃-refl) (resp-id p)) p
resp-is-equivalence′ :
∀ {a p r} {A : Set a}
(P : A → Set p) (R : A → A → Set r)
(≡↠R : ∀ {x y} → (x ≡ y) ↠ R x y)
(resp : ∀ {x y} → R x y → P x → P y) →
(∀ x p → resp (_↠_.to ≡↠R (refl x)) p ≡ p) →
∀ {x y} (r : R x y) → Is-equivalence (resp r)
resp-is-equivalence′ P R ≡↠R resp hyp r =
Eq.respects-extensional-equality
(λ p → sym $ transport-theorem′ P R ≡↠R resp hyp r p)
(subst-is-equivalence P (_↠_.from ≡↠R r))
≃⇒≡-→-cong :
∀ {ℓ} {A₁ A₂ B₁ B₂ : Set ℓ}
(ext : Extensionality ℓ ℓ) →
(univ : Univalence ℓ)
(A₁≃A₂ : A₁ ≃ A₂) (B₁≃B₂ : B₁ ≃ B₂) →
≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂) ≡
cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂)
≃⇒≡-→-cong {A₂ = A₂} {B₁} ext univ A₁≃A₂ B₁≃B₂ =
≃⇒≡ univ (→-cong ext A₁≃A₂ B₁≃B₂) ≡⟨ cong (≃⇒≡ univ) (lift-equality ext lemma) ⟩
≃⇒≡ univ (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
(≃⇒≡ univ B₁≃B₂))) ≡⟨ left-inverse-of (≡≃≃ univ) _ ⟩∎
cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂) (≃⇒≡ univ B₁≃B₂) ∎
where
open _≃_
lemma :
(λ f → to B₁≃B₂ ∘ f ∘ from A₁≃A₂) ≡
to (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
(≃⇒≡ univ B₁≃B₂)))
lemma =
(λ f → to B₁≃B₂ ∘ f ∘ from A₁≃A₂) ≡⟨ ext (λ _ → transport-theorem (λ B → A₂ → B) (λ A≃B g → _≃_.to A≃B ∘ g)
refl univ B₁≃B₂ _) ⟩
subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂) ∘
(λ f → f ∘ from A₁≃A₂) ≡⟨ cong (_∘_ (subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂))) (ext λ f →
transport-theorem (λ A → A → B₁) (λ A≃B g → g ∘ _≃_.from A≃B) refl univ A₁≃A₂ f) ⟩
subst (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂) ∘
subst (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂) ≡⟨ cong₂ (λ g h f → g (h f)) (ext $ subst-in-terms-of-≡⇒↝ equivalence _ (λ B → A₂ → B))
(ext $ subst-in-terms-of-≡⇒↝ equivalence _ (λ A → A → B₁)) ⟩
to (≡⇒≃ (cong (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂))) ∘
to (≡⇒≃ (cong (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂))) ≡⟨⟩
to (≡⇒≃ (cong (λ B → A₂ → B) (≃⇒≡ univ B₁≃B₂)) ⊚
≡⇒≃ (cong (λ A → A → B₁) (≃⇒≡ univ A₁≃A₂))) ≡⟨ cong to $ sym $ ≡⇒≃-trans ext _ _ ⟩∎
to (≡⇒≃ (cong₂ (λ A B → A → B) (≃⇒≡ univ A₁≃A₂)
(≃⇒≡ univ B₁≃B₂))) ∎
cong-≃⇒≡ :
∀ {ℓ p} {A B : Set ℓ} {A≃B : A ≃ B} →
Extensionality p p →
(univ₁ : Univalence ℓ)
(univ₂ : Univalence p)
(P : Set ℓ → Set p)
(P-cong : ∀ {A B} → A ≃ B → P A ≃ P B) →
(∀ {A} (p : P A) → _≃_.to (P-cong Eq.id) p ≡ p) →
cong P (≃⇒≡ univ₁ A≃B) ≡ ≃⇒≡ univ₂ (P-cong A≃B)
cong-≃⇒≡ {A≃B = A≃B} ext univ₁ univ₂ P P-cong P-cong-id =
cong P (≃⇒≡ univ₁ A≃B) ≡⟨ sym $ _≃_.left-inverse-of (≡≃≃ univ₂) _ ⟩
≃⇒≡ univ₂ (≡⇒≃ (cong P (≃⇒≡ univ₁ A≃B))) ≡⟨ cong (≃⇒≡ univ₂) $ lift-equality ext lemma ⟩∎
≃⇒≡ univ₂ (P-cong A≃B) ∎
where
lemma : ≡⇒→ (cong P (≃⇒≡ univ₁ A≃B)) ≡ _≃_.to (P-cong A≃B)
lemma = ext λ x →
≡⇒→ (cong P (≃⇒≡ univ₁ A≃B)) x ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence _ P x ⟩
subst P (≃⇒≡ univ₁ A≃B) x ≡⟨ sym $ transport-theorem P (_≃_.to ∘ P-cong) P-cong-id univ₁ A≃B x ⟩∎
_≃_.to (P-cong A≃B) x ∎
resp-preserves-compositions :
∀ {p₁ p₂} (P : Set p₁ → Set p₂) →
(resp : ∀ {A B} → A ≃ B → P A → P B) →
(∀ {A} (p : P A) → resp Eq.id p ≡ p) →
Univalence p₁ → Extensionality p₁ p₁ →
∀ {A B C} (A≃B : A ≃ B) (B≃C : B ≃ C) p →
resp (B≃C ⊚ A≃B) p ≡ (resp B≃C ∘ resp A≃B) p
resp-preserves-compositions P resp resp-id univ ext A≃B B≃C p =
resp (B≃C ⊚ A≃B) p ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
subst P (≃⇒≡ univ (B≃C ⊚ A≃B)) p ≡⟨ cong (λ eq → subst P eq p) $ ≃⇒≡-∘ univ ext A≃B B≃C ⟩
subst P (trans (≃⇒≡ univ A≃B) (≃⇒≡ univ B≃C)) p ≡⟨ sym $ subst-subst P _ _ _ ⟩
subst P (≃⇒≡ univ B≃C) (subst P (≃⇒≡ univ A≃B) p) ≡⟨ sym $ transport-theorem P resp resp-id univ _ _ ⟩
resp B≃C (subst P (≃⇒≡ univ A≃B) p) ≡⟨ sym $ cong (resp _) $ transport-theorem P resp resp-id univ _ _ ⟩∎
resp B≃C (resp A≃B p) ∎
resp-preserves-inverses :
∀ {p₁ p₂} (P : Set p₁ → Set p₂) →
(resp : ∀ {A B} → A ≃ B → P A → P B) →
(∀ {A} (p : P A) → resp Eq.id p ≡ p) →
Univalence p₁ → Extensionality p₁ p₁ →
∀ {A B} (A≃B : A ≃ B) p q →
resp A≃B p ≡ q → resp (inverse A≃B) q ≡ p
resp-preserves-inverses P resp resp-id univ ext A≃B p q eq =
let lemma =
q ≡⟨ sym eq ⟩
resp A≃B p ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
subst P (≃⇒≡ univ A≃B) p ≡⟨ cong (λ eq → subst P eq p) $ sym $ sym-sym _ ⟩∎
subst P (sym (sym (≃⇒≡ univ A≃B))) p ∎
in
resp (inverse A≃B) q ≡⟨ transport-theorem P resp resp-id univ _ _ ⟩
subst P (≃⇒≡ univ (inverse A≃B)) q ≡⟨ cong (λ eq → subst P eq q) $ ≃⇒≡-inverse univ ext A≃B ⟩
subst P (sym (≃⇒≡ univ A≃B)) q ≡⟨ cong (subst P (sym (≃⇒≡ univ A≃B))) lemma ⟩
subst P (sym (≃⇒≡ univ A≃B)) (subst P (sym (sym (≃⇒≡ univ A≃B))) p) ≡⟨ subst-subst-sym P _ _ ⟩∎
p ∎
≡-preserves-≃ :
∀ {ℓ₁ ℓ₂} {A₁ : Set ℓ₁} {A₂ : Set ℓ₂} {B₁ : Set ℓ₁} {B₂ : Set ℓ₂} →
Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
Univalence′ A₁ B₁ →
Univalence′ A₂ B₂ →
A₁ ≃ A₂ → B₁ ≃ B₂ → (A₁ ≡ B₁) ≃ (A₂ ≡ B₂)
≡-preserves-≃ {ℓ₁} {ℓ₂} {A₁} {A₂} {B₁} {B₂}
ext univ₁ univ₂ A₁≃A₂ B₁≃B₂ = ↔⇒≃ (record
{ surjection = record
{ logical-equivalence = record
{ to = to
; from = from
}
; right-inverse-of = to∘from
}
; left-inverse-of = from∘to
})
where
to = λ A₁≡B₁ → ≃⇒≡ univ₂ (
A₂ ↝⟨ inverse A₁≃A₂ ⟩
A₁ ↝⟨ ≡⇒≃ A₁≡B₁ ⟩
B₁ ↝⟨ B₁≃B₂ ⟩□
B₂ □)
from = λ A₂≡B₂ → ≃⇒≡ univ₁ (
A₁ ↝⟨ A₁≃A₂ ⟩
A₂ ↝⟨ ≡⇒≃ A₂≡B₂ ⟩
B₂ ↝⟨ inverse B₁≃B₂ ⟩□
B₁ □)
abstract
to∘from : ∀ eq → to (from eq) ≡ eq
to∘from A₂≡B₂ =
let ext₂ = lower-extensionality ℓ₁ ℓ₁ ext in
_≃_.to (≃-≡ (≡≃≃ univ₂)) (lift-equality ext₂ (
≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚ ≡⇒≃ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚
≡⇒≃ A₂≡B₂) ⊚ A₁≃A₂))) ⊚ inverse A₁≃A₂)) ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₂) _ ⟩
(_≃_.to B₁≃B₂ ∘
≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚ ≡⇒≃ A₂≡B₂) ⊚ A₁≃A₂)) ∘
_≃_.from A₁≃A₂) ≡⟨ cong (λ eq → _≃_.to B₁≃B₂ ∘ _≃_.to eq ∘ _≃_.from A₁≃A₂) $
_≃_.right-inverse-of (≡≃≃ univ₁) _ ⟩
((_≃_.to B₁≃B₂ ∘ _≃_.from B₁≃B₂) ∘ ≡⇒→ A₂≡B₂ ∘
(_≃_.to A₁≃A₂ ∘ _≃_.from A₁≃A₂)) ≡⟨ cong₂ (λ f g → f ∘ ≡⇒→ A₂≡B₂ ∘ g)
(ext₂ $ _≃_.right-inverse-of B₁≃B₂)
(ext₂ $ _≃_.right-inverse-of A₁≃A₂) ⟩∎
≡⇒→ A₂≡B₂ ∎))
from∘to : ∀ eq → from (to eq) ≡ eq
from∘to A₁≡B₁ =
let ext₁ = lower-extensionality ℓ₂ ℓ₂ ext in
_≃_.to (≃-≡ (≡≃≃ univ₁)) (lift-equality ext₁ (
≡⇒→ (≃⇒≡ univ₁ ((inverse B₁≃B₂ ⊚ ≡⇒≃ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚
≡⇒≃ A₁≡B₁) ⊚ inverse A₁≃A₂))) ⊚ A₁≃A₂)) ≡⟨ cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ₁) _ ⟩
(_≃_.from B₁≃B₂ ∘
≡⇒→ (≃⇒≡ univ₂ ((B₁≃B₂ ⊚ ≡⇒≃ A₁≡B₁) ⊚ inverse A₁≃A₂)) ∘
_≃_.to A₁≃A₂) ≡⟨ cong (λ eq → _≃_.from B₁≃B₂ ∘ _≃_.to eq ∘ _≃_.to A₁≃A₂) $
_≃_.right-inverse-of (≡≃≃ univ₂) _ ⟩
((_≃_.from B₁≃B₂ ∘ _≃_.to B₁≃B₂) ∘ ≡⇒→ A₁≡B₁ ∘
(_≃_.from A₁≃A₂ ∘ _≃_.to A₁≃A₂)) ≡⟨ cong₂ (λ f g → f ∘ ≡⇒→ A₁≡B₁ ∘ g)
(ext₁ $ _≃_.left-inverse-of B₁≃B₂)
(ext₁ $ _≃_.left-inverse-of A₁≃A₂) ⟩∎
≡⇒→ A₁≡B₁ ∎))
singleton-with-≃-↔-⊤ :
∀ {a b} {B : Set b} →
Extensionality (a ⊔ b) (a ⊔ b) →
Univalence (a ⊔ b) →
(∃ λ (A : Set (a ⊔ b)) → A ≃ B) ↔ ⊤
singleton-with-≃-↔-⊤ {a} {B = B} ext univ =
(∃ λ A → A ≃ B) ↝⟨ inverse (∃-cong λ _ → Eq.≃-preserves-bijections ext F.id Bijection.↑↔) ⟩
(∃ λ A → A ≃ ↑ a B) ↔⟨ inverse (∃-cong λ _ → ≡≃≃ univ) ⟩
(∃ λ A → A ≡ ↑ a B) ↝⟨ inverse $ _⇔_.to contractible⇔⊤↔ (singleton-contractible _) ⟩□
⊤ □
other-singleton-with-≃-↔-⊤ :
∀ {a b} {A : Set a} →
Extensionality (a ⊔ b) (a ⊔ b) →
Univalence (a ⊔ b) →
(∃ λ (B : Set (a ⊔ b)) → A ≃ B) ↔ ⊤
other-singleton-with-≃-↔-⊤ {b = b} {A} ext univ =
(∃ λ B → A ≃ B) ↝⟨ (∃-cong λ _ → inverse-isomorphism ext) ⟩
(∃ λ B → B ≃ A) ↝⟨ singleton-with-≃-↔-⊤ {a = b} ext univ ⟩□
⊤ □
∃Contractible↔⊤ :
∀ {a} →
Extensionality a a →
Univalence a →
(∃ λ (A : Set a) → Contractible A) ↔ ⊤
∃Contractible↔⊤ ext univ =
(∃ λ A → Contractible A) ↝⟨ (∃-cong λ _ → contractible↔⊤≃ ext) ⟩
(∃ λ A → ⊤ ≃ A) ↝⟨ other-singleton-with-≃-↔-⊤ ext univ ⟩
⊤ □
H-level-H-level-≡ :
∀ {a} {A₁ A₂ : Set a} →
Extensionality a a →
Univalence′ A₁ A₂ →
∀ n → H-level n A₁ → H-level n A₂ → H-level n (A₁ ≡ A₂)
H-level-H-level-≡ {A₁ = A₁} {A₂} ext univ n = curry (
H-level n A₁ × H-level n A₂ ↝⟨ uncurry (Eq.h-level-closure ext n) ⟩
H-level n (A₁ ≃ A₂) ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) n ⟩
H-level n (A₁ ≡ A₂) □)
H-level-H-level-≡ˡ :
∀ {a} {A₁ A₂ : Set a} →
Extensionality a a →
Univalence′ A₁ A₂ →
∀ n → H-level (1 + n) A₁ → H-level (1 + n) (A₁ ≡ A₂)
H-level-H-level-≡ˡ {A₁ = A₁} {A₂} ext univ n =
H-level (1 + n) A₁ ↝⟨ Eq.left-closure ext n ⟩
H-level (1 + n) (A₁ ≃ A₂) ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) ⟩
H-level (1 + n) (A₁ ≡ A₂) □
H-level-H-level-≡ʳ :
∀ {a} {A₁ A₂ : Set a} →
Extensionality a a →
Univalence′ A₁ A₂ →
∀ n → H-level (1 + n) A₂ → H-level (1 + n) (A₁ ≡ A₂)
H-level-H-level-≡ʳ {A₁ = A₁} {A₂} ext univ n =
H-level (1 + n) A₂ ↝⟨ Eq.right-closure ext n ⟩
H-level (1 + n) (A₁ ≃ A₂) ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≡≃≃ univ) (1 + n) ⟩
H-level (1 + n) (A₁ ≡ A₂) □
∃-H-level-H-level-1+ :
∀ {a} →
Extensionality a a →
Univalence a →
∀ n → H-level (1 + n) (∃ λ (A : Set a) → H-level n A)
∃-H-level-H-level-1+ ext univ n (A₁ , h₁) (A₂ , h₂) =
$⟨ h₁ , h₂ ⟩
H-level n A₁ × H-level n A₂ ↝⟨ uncurry (H-level-H-level-≡ ext univ n) ⟩
H-level n (A₁ ≡ A₂) ↝⟨ H-level.respects-surjection
(_↔_.surjection $ ignore-propositional-component
(H-level-propositional ext _)) n ⟩□
H-level n ((A₁ , h₁) ≡ (A₂ , h₂)) □
Is-set-∃-Is-proposition :
∀ {a} →
Extensionality (lsuc a) (lsuc a) →
Propositional-extensionality a →
Is-set (∃ λ (A : Set a) → Is-proposition A)
Is-set-∃-Is-proposition {a} ext prop-ext (A₁ , A₁-prop) (A₂ , A₂-prop) =
$⟨ _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
prop-ext A₁-prop A₂-prop ⟩
Univalence′ A₁ A₂ ↝⟨ (λ univ → H-level-H-level-≡ ext′ univ 1 A₁-prop A₂-prop) ⟩
Is-proposition (A₁ ≡ A₂) ↝⟨ H-level.respects-surjection
(_↔_.surjection $ ignore-propositional-component
(H-level-propositional ext′ _)) 1 ⟩□
Is-proposition ((A₁ , A₁-prop) ≡ (A₂ , A₂-prop)) □
where
ext′ = lower-extensionality _ _ ext
¬-∃-H-level-H-level :
∀ {a} →
∃ λ n → ¬ H-level n (∃ λ (A : Set a) → H-level n A)
¬-∃-H-level-H-level =
1 ,
( Is-proposition (∃ λ A → Is-proposition A) ↝⟨ _⇔_.to propositional⇔irrelevant ⟩
((p q : ∃ λ A → Is-proposition A) → p ≡ q) ↝⟨ (λ f p q → cong proj₁ (f p q)) ⟩
((p q : ∃ λ A → Is-proposition A) → proj₁ p ≡ proj₁ q) ↝⟨ (_$ (⊥ , ⊥-propositional)) ∘
(_$ (↑ _ ⊤ , ↑-closure 1 (mono₁ 0 ⊤-contractible))) ⟩
↑ _ ⊤ ≡ ⊥ ↝⟨ flip (subst id) _ ⟩
⊥ ↝⟨ ⊥-elim ⟩□
⊥₀ □)
∃¬↔⊤ :
∀ {a} →
Extensionality a a →
Univalence a →
(∃ λ (A : Set a) → ¬ A) ↔ ⊤
∃¬↔⊤ ext univ =
(∃ λ A → ¬ A) ↔⟨ inverse (∃-cong λ _ → ≃⊥≃¬ ext) ⟩
(∃ λ A → A ≃ ⊥₀) ↔⟨ singleton-with-≃-↔-⊤ ext univ ⟩
⊤ □
∃≢refl :
Extensionality (# 1) (# 1) →
Univalence (# 0) →
∃ λ (A : Set₁) → ∃ λ (f : (x : A) → x ≡ x) → f ≢ refl
∃≢refl ext univ =
(∃ λ (A : Set) → A ≡ A)
, _↔_.from iso f
, (_↔_.from iso f ≡ refl ↝⟨ cong (_↔_.to iso) ⟩
_↔_.to iso (_↔_.from iso f) ≡ _↔_.to iso refl ↝⟨ (λ eq → f ≡⟨ sym (_↔_.right-inverse-of iso f) ⟩
_↔_.to iso (_↔_.from iso f) ≡⟨ eq ⟩∎
_↔_.to iso refl ∎) ⟩
f ≡ _↔_.to iso refl ↝⟨ cong (λ f → proj₁ (f Bool (swap-as-an-equality univ))) ⟩
swap-as-an-equality univ ≡ proj₁ (_↔_.to iso refl Bool _) ↝⟨ (λ eq → swap-as-an-equality univ ≡⟨ eq ⟩
proj₁ (_↔_.to iso refl Bool _) ≡⟨ cong proj₁ Σ-≡,≡←≡-refl ⟩∎
refl Bool ∎) ⟩
swap-as-an-equality univ ≡ refl Bool ↝⟨ swap≢refl univ ⟩□
⊥ □)
where
f = λ A p → p , refl (trans p p)
iso =
((p : ∃ λ A → A ≡ A) → p ≡ p) ↝⟨ currying ⟩
(∀ A (p : A ≡ A) → (A , p) ≡ (A , p)) ↔⟨ (Eq.∀-preserves ext λ _ → Eq.∀-preserves ext λ _ →
Eq.↔⇒≃ $ inverse $ Bijection.Σ-≡,≡↔≡ {a = # 1}) ⟩
((A : Set) (p : A ≡ A) →
∃ λ (q : A ≡ A) → subst (λ A → A ≡ A) q p ≡ p) ↔⟨ (Eq.∀-preserves ext λ _ → Eq.∀-preserves ext λ _ →
∃-cong λ _ → ≡⇒↝ _ [subst≡]≡[trans≡trans]) ⟩□
((A : Set) (p : A ≡ A) →
∃ λ (q : A ≡ A) → trans p q ≡ trans q p) □
¬-type-of-refl-propositional :
Extensionality (# 1) (# 1) →
Univalence (# 0) →
∃ λ (A : Set₁) → ¬ Is-proposition ((a : A) → a ≡ a)
¬-type-of-refl-propositional ext univ =
let A , f , f≢refl = ∃≢refl ext univ in
A ,
(Is-proposition (∀ x → x ≡ x) ↝⟨ _⇔_.to propositional⇔irrelevant ⟩
Proof-irrelevant (∀ x → x ≡ x) ↝⟨ (λ irr → irr _ _) ⟩
f ≡ refl ↝⟨ f≢refl ⟩□
⊥ □)
¬-Set₁-groupoid :
Extensionality (# 1) (# 1) →
Univalence (# 1) →
Univalence (# 0) →
¬ H-level 3 Set₁
¬-Set₁-groupoid ext univ₁ univ₀ =
let L = _ in
H-level 3 Set₁ ↝⟨ (λ h → h _ _) ⟩
Is-set (L ≡ L) ↝⟨ H-level.respects-surjection (_≃_.surjection $ ≡≃≃ univ₁) 2 ⟩
Is-set (L ≃ L) ↝⟨ (λ h → h _ _) ⟩
Is-proposition (F.id ≡ F.id) ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ ≃-≡ $ ↔⇒≃ ≃-as-Σ) 1 ⟩
Is-proposition ((id , _) ≡ (id , _)) ↝⟨ H-level.respects-surjection
(_↔_.surjection $ inverse $ ignore-propositional-component (Eq.propositional ext id)) 1 ⟩
Is-proposition (id ≡ id) ↝⟨ H-level.respects-surjection (_≃_.surjection $ inverse $ extensionality-isomorphism ext) 1 ⟩
Is-proposition ((l : L) → l ≡ l) ↝⟨ proj₂ $ ¬-type-of-refl-propositional ext univ₀ ⟩□
⊥ □
≡↠⇔ : ∀ {ℓ} {A B : Set ℓ} →
Univalence′ A B →
Is-proposition A → Is-proposition B →
(A ≡ B) ↠ (A ⇔ B)
≡↠⇔ {A = A} {B} univ A-prop B-prop =
A ≡ B ↔⟨ ≡≃≃ univ ⟩
A ≃ B ↝⟨ ≃↠⇔ A-prop B-prop ⟩□
A ⇔ B □
⇔↔≡ : ∀ {ℓ} {A B : Set ℓ} →
Extensionality ℓ ℓ →
Univalence′ A B →
Is-proposition A → Is-proposition B →
(A ⇔ B) ↔ (A ≡ B)
⇔↔≡ {A = A} {B} ext univ A-prop B-prop =
A ⇔ B ↝⟨ ⇔↔≃ ext A-prop B-prop ⟩
A ≃ B ↔⟨ inverse $ ≡≃≃ univ ⟩□
A ≡ B □
⇔↔≡′ : ∀ {ℓ} {A B : Proposition ℓ} →
Extensionality ℓ ℓ →
Univalence′ (proj₁ A) (proj₁ B) →
(proj₁ A ⇔ proj₁ B) ↔ (A ≡ B)
⇔↔≡′ {A = A} {B} ext univ =
proj₁ A ⇔ proj₁ B ↝⟨ ⇔↔≡ ext univ (proj₂ A) (proj₂ B) ⟩
proj₁ A ≡ proj₁ B ↝⟨ ignore-propositional-component (H-level-propositional ext 1) ⟩□
A ≡ B □
⇔↔≡″ : ∀ {ℓ} {A B : Proposition ℓ} →
Extensionality (lsuc ℓ) (lsuc ℓ) →
Propositional-extensionality ℓ →
(proj₁ A ⇔ proj₁ B) ↔ (A ≡ B)
⇔↔≡″ {ℓ} {A} {B} ext =
Propositional-extensionality ℓ ↝⟨ (λ prop-ext → _≃_.to (Propositional-extensionality-is-univalence-for-propositions ext)
prop-ext (proj₂ A) (proj₂ B)) ⟩
Univalence′ (proj₁ A) (proj₁ B) ↝⟨ ⇔↔≡′ (lower-extensionality _ _ ext) ⟩□
(proj₁ A ⇔ proj₁ B) ↔ (A ≡ B) □