{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Pointed-type
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open Derived-definitions-and-properties eq
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (_×_)
open import Bijection eq as B using (_↔_)
open import Equivalence eq as E using (_≃_)
open import Extensionality eq
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq
open import Surjection eq using (_↠_)
open import Univalence-axiom eq
private
variable
a b ℓ : Level
A B : Type a
x y : A
p q : x ≡ y
k : Kind
Pointed-type : ∀ ℓ → Type (lsuc ℓ)
Pointed-type a = ∃ λ (A : Type a) → A
infix 4 _↝[_]ᴮ_ _→ᴮ_ _≃ᴮ_
_↝[_]ᴮ_ : Pointed-type a → Kind → Pointed-type b → Type (a ⊔ b)
(A , x) ↝[ k ]ᴮ (B , y) =
∃ λ (f : A ↝[ k ] B) → to-implication f x ≡ y
_→ᴮ_ : Pointed-type a → Pointed-type b → Type (a ⊔ b)
_→ᴮ_ = _↝[ implication ]ᴮ_
_≃ᴮ_ : Pointed-type a → Pointed-type b → Type (a ⊔ b)
_≃ᴮ_ = _↝[ equivalence ]ᴮ_
private
variable
P P₁ P₂ Q Q₁ Q₂ R : Pointed-type a
P→Q : P →ᴮ Q
P≃Q : P ≃ᴮ Q
≃ᴮ→→ᴮ : P ≃ᴮ Q → P →ᴮ Q
≃ᴮ→→ᴮ = Σ-map _≃_.to id
≃ᴮ≃≡ : {P Q : Pointed-type a} → Univalence a → (P ≃ᴮ Q) ≃ (P ≡ Q)
≃ᴮ≃≡ {P = A , x} {Q = B , y} univ =
(∃ λ (A≃B : A ≃ B) → _≃_.to A≃B x ≡ y) ↝⟨ (inverse $
Σ-cong (≡≃≃ univ) λ A≃B →
≡⇒≃ $ cong (_≡ _) $
subst-id-in-terms-of-≡⇒↝ equivalence) ⟩
(∃ λ (A≡B : A ≡ B) → subst id A≡B x ≡ y) ↔⟨ B.Σ-≡,≡↔≡ ⟩□
(A , x) ≡ (B , y) □
↝ᴮ-refl : P ↝[ k ]ᴮ P
↝ᴮ-refl {k} = F.id , cong (_$ _) (to-implication-id k)
↝ᴮ-trans : P ↝[ k ]ᴮ Q → Q ↝[ k ]ᴮ R → P ↝[ k ]ᴮ R
↝ᴮ-trans {P = _ , x} {k} {Q = _ , y} {R = _ , z}
(A↝B , p) (B↝C , q) =
B↝C F.∘ A↝B
, (to-implication (B↝C F.∘ A↝B) x ≡⟨ cong (_$ _) $ to-implication-∘ k ⟩
to-implication B↝C (to-implication A↝B x) ≡⟨ cong (to-implication B↝C) p ⟩
to-implication B↝C y ≡⟨ q ⟩∎
z ∎)
≃ᴮ-sym : P ≃ᴮ Q → Q ≃ᴮ P
≃ᴮ-sym (A≃B , p) = inverse A≃B , _≃_.to-from A≃B p
infix -1 _□ᴮ finallyᴮ
infixr -2 stepᴮ
stepᴮ : (P : Pointed-type a) {Q : Pointed-type b} →
Q ↝[ k ]ᴮ R → P ↝[ k ]ᴮ Q → P ↝[ k ]ᴮ R
stepᴮ _ = flip ↝ᴮ-trans
syntax stepᴮ P Q↝R P↝Q = P ↝ᴮ⟨ P↝Q ⟩ Q↝R
finallyᴮ :
(P : Pointed-type a) (Q : Pointed-type b) →
P ↝[ k ]ᴮ Q → P ↝[ k ]ᴮ Q
finallyᴮ _ _ P↝Q = P↝Q
syntax finallyᴮ P Q P↝Q = P ↝ᴮ⟨ P↝Q ⟩□ Q □
_□ᴮ : (P : Pointed-type a) → P ↝[ k ]ᴮ P
_ □ᴮ = ↝ᴮ-refl
Maybe→ᴮ↠→ : (Maybe A , nothing) →ᴮ (B , x) ↠ (A → B)
Maybe→ᴮ↠→ {A} {B} {x} = record
{ logical-equivalence = record
{ to = (Maybe A , nothing) →ᴮ (B , x) ↝⟨ proj₁ ⟩
(Maybe A → B) ↝⟨ _∘ inj₂ ⟩□
(A → B) □
; from = λ f → [ (λ _ → x) , f ] , refl x
}
; right-inverse-of = refl
}
Maybe→ᴮ↔→ :
∀ {A : Type a} {B : Type b} {x} →
(Maybe A , nothing) →ᴮ (B , x) ↝[ a ∣ b ] (A → B)
Maybe→ᴮ↔→ {A} {B} {x} = generalise-ext?
(_↠_.logical-equivalence Maybe→ᴮ↠→)
(λ ext →
refl
, (λ (f , eq) → Σ-≡,≡→≡
(apply-ext ext
[ (λ _ →
x ≡⟨ sym eq ⟩∎
f nothing ∎)
, (λ _ → refl _)
])
(subst (λ f → f nothing ≡ x)
(apply-ext ext [ (λ _ → sym eq) , (λ _ → refl _) ])
(refl x) ≡⟨ subst-ext ext ⟩
subst (_≡ x) (sym eq) (refl x) ≡⟨ subst-trans _ ⟩
trans eq (refl x) ≡⟨ trans-reflʳ _ ⟩∎
eq ∎)))
Bool→ᴮ↔ :
∀ {A : Type a} {x} →
(Bool , true) →ᴮ (A , x) ↝[ lzero ∣ a ] A
Bool→ᴮ↔ {A} {x} ext =
(Bool , true) →ᴮ (A , x) ↝⟨ Maybe→ᴮ↔→ ext ⟩
(⊤ → A) ↔⟨ Π-left-identity ⟩□
A □
Ω : Pointed-type ℓ → Pointed-type ℓ
Ω (A , x) = (x ≡ x) , refl x
Ω[_] : ℕ → Pointed-type ℓ → Pointed-type ℓ
Ω[ zero ] = id
Ω[ suc n ] = Ω ∘ Ω[ n ]
Ω∘Ω[]≡Ω[]∘Ω : ∀ n → Ω (Ω[ n ] P) ≡ Ω[ n ] (Ω P)
Ω∘Ω[]≡Ω[]∘Ω {P} zero =
Ω P ∎
Ω∘Ω[]≡Ω[]∘Ω {P} (suc n) =
Ω (Ω[ suc n ] P) ≡⟨⟩
Ω (Ω (Ω[ n ] P)) ≡⟨ cong Ω $ Ω∘Ω[]≡Ω[]∘Ω n ⟩
Ω (Ω[ n ] (Ω P)) ≡⟨⟩
Ω[ suc n ] (Ω P) ∎
Ω-cong-→ᴮ : P →ᴮ Q → Ω P →ᴮ Ω Q
Ω-cong-→ᴮ {P = A , x} {Q = B , y} (to , to≡) =
(x ≡ x ↝⟨ cong to ⟩
to x ≡ to x ↔⟨ ≡⇒≃ $ cong₂ _≡_ to≡ to≡ ⟩□
y ≡ y □)
, (≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to (refl x)) ≡⟨ cong (≡⇒→ (cong₂ _≡_ to≡ to≡)) $ cong-refl _ ⟩
≡⇒→ (cong₂ _≡_ to≡ to≡) (refl (to x)) ≡⟨ elim¹
(λ to≡ → ≡⇒→ (cong₂ _≡_ to≡ to≡) (refl (to x)) ≡
refl _)
(
≡⇒→ (cong₂ _≡_ (refl _) (refl _)) (refl _) ≡⟨ cong (λ eq → ≡⇒→ eq (refl _)) $ cong₂-refl _≡_ ⟩
≡⇒→ (refl _) (refl _) ≡⟨ cong (λ eq → _≃_.to eq (refl _)) ≡⇒↝-refl ⟩∎
refl _ ∎)
_ ⟩∎
refl y ∎)
Ω-cong-≃ᴮ : P ≃ᴮ Q → Ω P ≃ᴮ Ω Q
Ω-cong-≃ᴮ {P = A , x} {Q = B , y} (A≃B , to≡) =
(x ≡ x ↝⟨ inverse $ E.≃-≡ A≃B ⟩
_≃_.to A≃B x ≡ _≃_.to A≃B x ↝⟨ ≡⇒↝ _ $ cong₂ _≡_ to≡ to≡ ⟩□
y ≡ y □)
, proj₂ (Ω-cong-→ᴮ (_≃_.to A≃B , to≡))
Ω[_]-cong-→ᴮ : ∀ n → P →ᴮ Q → Ω[ n ] P →ᴮ Ω[ n ] Q
Ω[ zero ]-cong-→ᴮ A→B = A→B
Ω[ suc n ]-cong-→ᴮ A→B = Ω-cong-→ᴮ (Ω[ n ]-cong-→ᴮ A→B)
Ω[_]-cong-≃ᴮ : ∀ n → P ≃ᴮ Q → Ω[ n ] P ≃ᴮ Ω[ n ] Q
Ω[ zero ]-cong-≃ᴮ A≃B = A≃B
Ω[ suc n ]-cong-≃ᴮ A≃B = Ω-cong-≃ᴮ (Ω[ n ]-cong-≃ᴮ A≃B)
≃ᴮ→→ᴮ-Ω-cong-≃ᴮ :
(P≃Q : P ≃ᴮ Q) →
≃ᴮ→→ᴮ (Ω-cong-≃ᴮ P≃Q) ≡ Ω-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q)
≃ᴮ→→ᴮ-Ω-cong-≃ᴮ _ = refl _
≃ᴮ→→ᴮ-Ω[_]-cong-≃ᴮ :
∀ n →
≃ᴮ→→ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q) ≡
Ω[ n ]-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q)
≃ᴮ→→ᴮ-Ω[_]-cong-≃ᴮ {P≃Q} = λ where
zero → refl _
(suc n) →
≃ᴮ→→ᴮ (Ω-cong-≃ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q)) ≡⟨⟩
Ω-cong-→ᴮ (≃ᴮ→→ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q)) ≡⟨ cong Ω-cong-→ᴮ ≃ᴮ→→ᴮ-Ω[ n ]-cong-≃ᴮ ⟩
Ω-cong-→ᴮ (Ω[ n ]-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q)) ∎
proj₁-Ω-cong-→ᴮ-↝ᴮ-refl :
proj₁ (Ω-cong-→ᴮ ↝ᴮ-refl) p ≡ p
proj₁-Ω-cong-→ᴮ-↝ᴮ-refl {p} =
≡⇒→
(cong₂ _≡_
(cong (_$ _) (refl _))
(cong (_$ _) (refl _)))
(cong id p) ≡⟨ cong₂ ≡⇒→
(trans (cong₂ (cong₂ _≡_)
(cong-refl _)
(cong-refl _)) $
cong₂-refl _≡_)
(sym $ cong-id _) ⟩
≡⇒→ (refl _) p ≡⟨ cong (_$ _) ≡⇒→-refl ⟩∎
p ∎
proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl :
_≃_.to (proj₁ (Ω-cong-≃ᴮ ↝ᴮ-refl)) p ≡ p
proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl = proj₁-Ω-cong-→ᴮ-↝ᴮ-refl
Ω-cong-→ᴮ-trans :
proj₁ (Ω-cong-→ᴮ P→Q) (trans p q) ≡
trans (proj₁ (Ω-cong-→ᴮ P→Q) p)
(proj₁ (Ω-cong-→ᴮ P→Q) q)
Ω-cong-→ᴮ-trans {P→Q = to , to≡} {p} {q} =
≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to (trans p q)) ≡⟨ cong (≡⇒→ (cong₂ _≡_ to≡ to≡)) $
cong-trans _ _ _ ⟩
≡⇒→ (cong₂ _≡_ to≡ to≡)
(trans (cong to p) (cong to q)) ≡⟨ lemma _ ⟩
trans
(trans (sym to≡)
(trans (cong to p) (cong to q)))
to≡ ≡⟨ trans (cong (flip trans _) $ sym $ trans-assoc _ _ _) $
trans-assoc _ _ _ ⟩
trans
(trans (sym to≡) (cong to p))
(trans (cong to q) to≡) ≡⟨ cong (trans _) $ sym $
trans--[trans-sym] _ _ ⟩
trans (trans (sym to≡) (cong to p))
(trans to≡ (trans (sym to≡) (trans (cong to q) to≡))) ≡⟨ trans (cong (trans _) $ cong (trans _) $ sym $ trans-assoc _ _ _) $
sym $ trans-assoc _ _ _ ⟩
trans
(trans (trans (sym to≡) (cong to p)) to≡)
(trans (trans (sym to≡) (cong to q)) to≡) ≡⟨ sym $ cong₂ trans (lemma _) (lemma _) ⟩∎
trans
(≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to p))
(≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to q)) ∎
where
lemma = λ p →
≡⇒→ (cong₂ _≡_ to≡ to≡) p ≡⟨⟩
≡⇒→ (trans (cong (_≡ _) to≡) (cong (_ ≡_) to≡)) p ≡⟨ cong (_$ p) $ ≡⇒↝-trans equivalence ⟩
≡⇒→ (cong (_ ≡_) to≡) (≡⇒→ (cong (_≡ _) to≡) p) ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
subst (_ ≡_) to≡ (≡⇒→ (cong (_≡ _) to≡) p) ≡⟨ sym trans-subst ⟩
trans (≡⇒→ (cong (_≡ _) to≡) p) to≡ ≡⟨ cong (flip trans _) $ sym $ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
trans (subst (_≡ _) to≡ p) to≡ ≡⟨ cong (flip trans _) subst-trans-sym ⟩∎
trans (trans (sym to≡) p) to≡ ∎
Ω-cong-≃ᴮ-trans :
(P≃Q : P ≃ᴮ Q) →
_≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) (trans p q) ≡
trans (_≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) p)
(_≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) q)
Ω-cong-≃ᴮ-trans _ = Ω-cong-→ᴮ-trans
Ω[1+_]-cong-→ᴮ-trans :
∀ n {p q} →
proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) (trans p q) ≡
trans (proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) p)
(proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) q)
Ω[1+ _ ]-cong-→ᴮ-trans = Ω-cong-→ᴮ-trans
Ω[1+_]-cong-≃ᴮ-trans :
∀ n {p q} (P≃Q : P ≃ᴮ Q) →
_≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) (trans p q) ≡
trans (_≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) p)
(_≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) q)
Ω[1+ n ]-cong-≃ᴮ-trans P≃Q = Ω-cong-≃ᴮ-trans (Ω[ n ]-cong-≃ᴮ P≃Q)
+⇔∀contractible-Ω[] :
∀ n →
H-level (1 + n) A
⇔
((x : A) → Contractible (proj₁ $ Ω[ n ] (A , x)))
+⇔∀contractible-Ω[] {A} zero =
Is-proposition A ↝⟨ record { to = propositional⇒inhabited⇒contractible
; from = [inhabited⇒contractible]⇒propositional
} ⟩□
(A → Contractible A) □
+⇔∀contractible-Ω[] {A} (suc zero) =
Is-set A ↝⟨ 2+⇔∀1+≡ 0 ⟩
((x : A) → Is-proposition (x ≡ x)) ↝⟨ (∀-cong _ λ x → record { to = flip propositional⇒inhabited⇒contractible (refl x)
; from = mono₁ 0
}) ⟩□
((x : A) → Contractible (x ≡ x)) □
+⇔∀contractible-Ω[] {A} (suc (suc n)) =
H-level (3 + n) A ↝⟨ 2+⇔∀1+≡ (1 + n) ⟩
((x : A) → H-level (2 + n) (x ≡ x)) ↝⟨ (∀-cong _ λ _ → +⇔∀contractible-Ω[] (suc n)) ⟩
((x : A) (p : x ≡ x) →
Contractible (proj₁ $ Ω[ 1 + n ] ((x ≡ x) , p))) ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → H-level-cong _ _ $ proj₁ $
Ω[ 1 + n ]-cong-≃ᴮ $ lemma _) ⟩
((x : A) → x ≡ x → Contractible (proj₁ $ Ω[ 1 + n ] (Ω (A , x)))) ↝⟨ (∀-cong _ λ x → _↠_.logical-equivalence $ inhabited→↠ (refl x)) ⟩
((x : A) → Contractible (proj₁ $ Ω[ 1 + n ] (Ω (A , x)))) ↝⟨ (∀-cong _ λ _ → ≡⇒↝ _ $ cong (Contractible ∘ proj₁) $ sym $
Ω∘Ω[]≡Ω[]∘Ω (1 + n)) ⟩□
((x : A) → Contractible (proj₁ $ Ω[ 2 + n ] (A , x))) □
where
lemma : (p : x ≡ x) → ((x ≡ x) , p) ≃ᴮ Ω (A , x)
lemma p = E.↔⇒≃ (inverse $ flip-trans-isomorphism p)
, (trans p (sym p) ≡⟨ trans-symʳ _ ⟩∎
refl _ ∎)
infixr 2 _×_
_×_ : Pointed-type a → Pointed-type b → Pointed-type (a ⊔ b)
(A , x) × (B , y) = (A P.× B) , (x , y)
proj₁ᴾ : (P × Q) →ᴮ P
proj₁ᴾ = proj₁ , refl _
proj₂ᴾ : (P × Q) →ᴮ Q
proj₂ᴾ = proj₂ , refl _
infixr 2 _×-cong-→ᴮ_ _×-cong-≃ᴮ_
_×-cong-→ᴮ_ : P₁ →ᴮ P₂ → Q₁ →ᴮ Q₂ → (P₁ × Q₁) →ᴮ (P₂ × Q₂)
(f₁ , eq₁) ×-cong-→ᴮ (f₂ , eq₂) =
(f₁ ×-cong f₂)
, cong₂ _,_ eq₁ eq₂
_×-cong-≃ᴮ_ : P₁ ≃ᴮ P₂ → Q₁ ≃ᴮ Q₂ → (P₁ × Q₁) ≃ᴮ (P₂ × Q₂)
(f₁ , eq₁) ×-cong-≃ᴮ (f₂ , eq₂) =
(f₁ ×-cong f₂)
, cong₂ _,_ eq₁ eq₂
Ω-× : Ω (P × Q) ≃ᴮ (Ω P × Ω Q)
Ω-× {P = A , x} {Q = B , y} =
((x , y) ≡ (x , y) ↝⟨ E.↔⇒≃ (inverse ≡×≡↔≡) ⟩□
x ≡ x P.× y ≡ y □)
, ((cong proj₁ (refl (x , y)) , cong proj₂ (refl (x , y))) ≡⟨ cong₂ _,_ (cong-refl _) (cong-refl _) ⟩∎
(refl x , refl y) ∎)
Ω[_]-× : ∀ n → Ω[ n ] (P × Q) ≃ᴮ (Ω[ n ] P × Ω[ n ] Q)
Ω[_]-× {P} {Q} = λ where
zero → P × Q □ᴮ
(suc n) →
Ω (Ω[ n ] (P × Q)) ↝ᴮ⟨ Ω-cong-≃ᴮ Ω[ n ]-× ⟩
Ω (Ω[ n ] P × Ω[ n ] Q) ↝ᴮ⟨ Ω-× ⟩□
Ω (Ω[ n ] P) × Ω (Ω[ n ] Q) □
Ω[1]-× : _≃_.to (proj₁ Ω[ 1 ]-×) p ≡ _≃_.to (proj₁ Ω-×) p
Ω[1]-× {p} =
_≃_.to (proj₁ Ω[ 1 ]-×) p ≡⟨⟩
_≃_.to (proj₁ Ω-×) (_≃_.to (proj₁ (Ω-cong-≃ᴮ ↝ᴮ-refl)) p) ≡⟨ cong (_≃_.to (proj₁ Ω-×)) proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl ⟩∎
_≃_.to (proj₁ Ω-×) p ∎
Ω-×-trans :
_≃_.to (proj₁ Ω-×) (trans p q) ≡
Σ-zip trans trans
(_≃_.to (proj₁ Ω-×) p)
(_≃_.to (proj₁ Ω-×) q)
Ω-×-trans {p} {q} =
_≃_.to (proj₁ Ω-×) (trans p q) ≡⟨⟩
( cong proj₁ (trans p q)
, cong proj₂ (trans p q)
) ≡⟨ cong₂ _,_
(cong-trans _ _ _)
(cong-trans _ _ _) ⟩
( trans (cong proj₁ p) (cong proj₁ q)
, trans (cong proj₂ p) (cong proj₂ q)
) ≡⟨⟩
Σ-zip trans trans
(_≃_.to (proj₁ Ω-×) p)
(_≃_.to (proj₁ Ω-×) q) ∎
Ω[1+_]-×-trans :
∀ n {p q : proj₁ (Ω[ suc n ] (P × Q))} →
_≃_.to (proj₁ Ω[ suc n ]-×) (trans p q) ≡
Σ-zip trans trans
(_≃_.to (proj₁ Ω[ suc n ]-×) p)
(_≃_.to (proj₁ Ω[ suc n ]-×) q)
Ω[1+ n ]-×-trans {p} {q} =
_≃_.to (proj₁ Ω-×)
(_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) (trans p q)) ≡⟨ cong (_≃_.to (proj₁ Ω-×)) $ Ω-cong-≃ᴮ-trans Ω[ n ]-× ⟩
_≃_.to (proj₁ Ω-×)
(trans (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) p)
(_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) q)) ≡⟨ Ω-×-trans ⟩∎
Σ-zip trans trans
(_≃_.to (proj₁ Ω-×)
(_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) p))
(_≃_.to (proj₁ Ω-×)
(_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) q)) ∎