{-# OPTIONS --cubical --safe #-}
module Equality.Path.Univalence where
open import Agda.Builtin.Cubical.Glue as Glue hiding (_≃_)
open import Equality.Path
open import Prelude
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence.Contractible-preimages equality-with-J as CP
import Equivalence.Half-adjoint equality-with-J as HA
open import Function-universe equality-with-J hiding (id)
open import H-level.Closure equality-with-J
open import Preimage equality-with-J
open import Univalence-axiom equality-with-J hiding (≃⇒≡)
private
variable
a b ℓ : Level
A : Type a
private
≃-CP⇒≃-Glue : {B : Type b} → A CP.≃ B → A Glue.≃ B
≃-CP⇒≃-Glue = Σ-map id (λ eq → record { equiv-proof = eq })
≃-Glue⇒≃-CP : {B : Type b} → A Glue.≃ B → A CP.≃ B
≃-Glue⇒≃-CP = Σ-map id Glue.isEquiv.equiv-proof
≃-CP⇒≡ : {A B : Type ℓ} → A CP.≃ B → A ≡ B
≃-CP⇒≡ {A} {B} A≃B = λ i → primGlue B
(λ { (i = 0̲) → A
; (i = 1̲) → B
})
(λ { (i = 0̲) → ≃-CP⇒≃-Glue A≃B
; (i = 1̲) → ≃-CP⇒≃-Glue CP.id
})
≃-CP⇒≡-id : ≃-CP⇒≡ CP.id ≡ refl {x = A}
≃-CP⇒≡-id {A} = λ i j → primGlue A
{φ = max i (max j (- j))}
(λ _ → A)
(λ _ → ≃-CP⇒≃-Glue CP.id)
≃-CP⇒≡∘≡⇒≃ :
{A B : Type ℓ} (A≡B : A ≡ B) →
≃-CP⇒≡ (CP.≡⇒≃ A≡B) ≡ A≡B
≃-CP⇒≡∘≡⇒≃ = elim
(λ A≡B → ≃-CP⇒≡ (CP.≡⇒≃ A≡B) ≡ A≡B)
(λ A →
≃-CP⇒≡ (CP.≡⇒≃ refl) ≡⟨ cong ≃-CP⇒≡ CP.≡⇒≃-refl ⟩
≃-CP⇒≡ CP.id ≡⟨ ≃-CP⇒≡-id ⟩∎
refl ∎)
≡⇒≃∘≃-CP⇒≡ :
{A B : Type ℓ} (A≃B : A CP.≃ B) →
CP.≡⇒≃ (≃-CP⇒≡ A≃B) ≡ A≃B
≡⇒≃∘≃-CP⇒≡ {A} {B} A≃B =
Σ-≡,≡→≡
(proj₁ (CP.≡⇒≃ (≃-CP⇒≡ A≃B)) ≡⟨⟩
proj₁ (transport (λ i → A CP.≃ ≃-CP⇒≡ A≃B i) 0̲ CP.id) ≡⟨⟩
transport (λ i → A → ≃-CP⇒≡ A≃B i) 0̲ id ≡⟨⟩
transport (λ _ → A → B) 0̲ (proj₁ A≃B) ≡⟨ cong (_$ proj₁ A≃B) $ transport-refl 0̲ ⟩∎
proj₁ A≃B ∎)
(Is-equivalence-CP-propositional ext _ _)
univ-CP : CP.Univalence ℓ
univ-CP =
Is-equivalence≃Is-equivalence-CP _ $
_≃_.is-equivalence $
Eq.↔→≃ _ ≃-CP⇒≡ ≡⇒≃∘≃-CP⇒≡ ≃-CP⇒≡∘≡⇒≃
univ : ∀ {ℓ} → Univalence ℓ
univ {A} {B} = record
{ univalence = from , proofs
}
where
univ′ : Univalence′ A B
univ′ = _≃_.from (Univalence≃Univalence-CP ext) univ-CP
from : A ≃ B → A ≡ B
from = proj₁ (Univalence′.univalence univ′)
opaque
proofs : HA.Proofs ≡⇒≃ from
proofs = proj₂ (Univalence′.univalence univ′)
≃⇒≡ : {A B : Type ℓ} → A ≃ B → A ≡ B
≃⇒≡ = _≃_.from Eq.⟨ _ , Univalence′.univalence univ ⟩
private
primGlue≃-CP :
(φ : I)
(B : Partial φ (Type ℓ))
(f : PartialP φ (λ x → B x Glue.≃ A)) →
primGlue A B f CP.≃ A
primGlue≃-CP {A} φ B f =
prim^unglue {φ = φ}
, λ x →
( prim^glue
(λ p → CP.inverse (proj₂ (f-CP p)) x)
(hcomp (lemma₁ x) x)
, (hcomp (lemma₁ x) x ≡⟨ sym $ hfill (lemma₁ x) (inˢ x) ⟩∎
x ∎)
)
, λ y i →
prim^glue (λ { (φ = 1̲) → proj₁ (lemma₂ is-one y i) })
(hcomp (lemma₃ y i) x)
, (hcomp (lemma₃ y i) x ≡⟨ sym $ hfill (lemma₃ y i) (inˢ x) ⟩∎
x ∎)
where
f-CP : PartialP φ (λ x → B x CP.≃ A)
f-CP p = ≃-Glue⇒≃-CP (f p)
lemma₁ : A → ∀ i → Partial φ A
lemma₁ x i (φ = 1̲) = (
x ≡⟨ sym (CP.right-inverse-of (proj₂ (f-CP is-one)) x) ⟩∎
proj₁ (f-CP _) (CP.inverse (proj₂ (f-CP _)) x) ∎) i
lemma₂ :
∀ {x} p (y : proj₁ (f-CP p) ⁻¹ x) →
( CP.inverse (proj₂ (f-CP p)) x
, CP.right-inverse-of (proj₂ (f-CP p)) x
) ≡
y
lemma₂ {x} p = CP.irrelevance (proj₂ (f-CP p)) x
lemma₃ : ∀ {x} → prim^unglue {e = f} ⁻¹ x →
∀ i → I → Partial (max φ (max i (- i))) A
lemma₃ y i j (φ = 1̲) = sym (proj₂ (lemma₂ is-one y i)) j
lemma₃ {x} _ i j (i = 0̲) = hfill (lemma₁ x) (inˢ x) j
lemma₃ y i j (i = 1̲) = sym (proj₂ y) j
other-univ : Other-univalence ℓ
other-univ {ℓ} {B} = $⟨ other-univ-CP ⟩
Contractible (∃ λ (A : Type ℓ) → A CP.≃ B) ↝⟨ (H-level-cong _ 0 $
∃-cong λ _ → inverse $
≃≃≃-CP {k = equivalence} ext) ⦂ (_ → _) ⟩□
Contractible (∃ λ (A : Type ℓ) → A ≃ B) □
where
other-univ-CP : Contractible (∃ λ (A : Type ℓ) → A CP.≃ B)
other-univ-CP =
(B , CP.id)
, λ (A , A≃B) i →
let C : ∀ i → Partial (max i (- i)) (Type ℓ)
C = λ { i (i = 0̲) → B
; i (i = 1̲) → A
}
f : ∀ i → PartialP (max i (- i)) (λ j → C i j Glue.≃ B)
f = λ { i (i = 0̲) → ≃-CP⇒≃-Glue CP.id
; i (i = 1̲) → ≃-CP⇒≃-Glue A≃B
}
in
primGlue _ _ (f i)
, primGlue≃-CP _ _ (f i)