{-# OPTIONS --erased-cubical --safe #-}
import Equality.Path as P
module Circle {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
open P.Derived-definitions-and-properties eq hiding (elim)
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Bijection equality-with-J as Bijection using (_↔_)
import Bijection P.equality-with-J as PB
open import Double-negation equality-with-J as DN
using (¬¬_; ¬¬-modality)
open import Equality.Groupoid equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
import Equality.Path.Isomorphisms P.equality-with-paths as PI
open import Equality.Tactic equality-with-J hiding (module Eq)
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PE
import Erased.Cubical eq as E
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Group equality-with-J as G using (_≃ᴳ_)
import Group.Cyclic eq as C
open import Groupoid equality-with-J
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation eq as T using (∥_∥[1+_])
open import H-level.Truncation.Propositional eq as Trunc
using (∥_∥; ∣_∣)
open import H-level.Truncation.Propositional.One-step eq as O
using (∥_∥¹)
open import Integer equality-with-J as Int
using (ℤ; +_; -[1+_]; ℤ-group)
open import Modality equality-with-J
open import Nat equality-with-J
open import Pointed-type equality-with-J as PT using (_≃ᴮ_)
open import Pointed-type.Homotopy-group eq
open import Sphere eq as Sphere using (𝕊)
open import Suspension eq as Suspension
using (Susp; north; south; meridian)
open import Univalence-axiom equality-with-J as Univ using (Univalence)
private
variable
a p : Level
A : Type p
P : A → Type p
f : (x : A) → P x
b ℓ x : A
data 𝕊¹ : Type where
base : 𝕊¹
loopᴾ : base P.≡ base
loop : base ≡ base
loop = _↔_.from ≡↔≡ loopᴾ
elimᴾ :
(P : 𝕊¹ → Type p)
(b : P base) →
P.[ (λ i → P (loopᴾ i)) ] b ≡ b →
(x : 𝕊¹) → P x
elimᴾ P b ℓ base = b
elimᴾ P b ℓ (loopᴾ i) = ℓ i
recᴾ : (b : A) → b P.≡ b → 𝕊¹ → A
recᴾ = elimᴾ _
elim :
(P : 𝕊¹ → Type p)
(b : P base) →
subst P loop b ≡ b →
(x : 𝕊¹) → P x
elim P b ℓ = elimᴾ P b (subst≡→[]≡ ℓ)
elim-loop : dcong (elim P b ℓ) loop ≡ ℓ
elim-loop = dcong-subst≡→[]≡ (refl _)
η-elim :
{f : (x : 𝕊¹) → P x} →
f ≡ elim P (f base) (dcong f loop)
η-elim {P} {f} =
⟨ext⟩ $ elim _ (refl _)
(subst (λ x → f x ≡ elim P (f base) (dcong f loop) x) loop (refl _) ≡⟨ subst-in-terms-of-trans-and-dcong ⟩
trans (sym (dcong f loop))
(trans (cong (subst P loop) (refl _))
(dcong (elim P (f base) (dcong f loop)) loop)) ≡⟨ cong (trans (sym (dcong f loop))) $
trans (cong (flip trans _) $ cong-refl _) $
trans-reflˡ _ ⟩
trans (sym (dcong f loop))
(dcong (elim P (f base) (dcong f loop)) loop) ≡⟨ cong (trans (sym (dcong f loop))) elim-loop ⟩
trans (sym (dcong f loop)) (dcong f loop) ≡⟨ trans-symˡ _ ⟩∎
refl _ ∎)
rec : (b : A) → b ≡ b → 𝕊¹ → A
rec b ℓ = recᴾ b (_↔_.to ≡↔≡ ℓ)
rec-loop : cong (rec b ℓ) loop ≡ ℓ
rec-loop = cong-≡↔≡ (refl _)
η-rec : {f : 𝕊¹ → A} → f ≡ rec (f base) (cong f loop)
η-rec {f} =
⟨ext⟩ $ elim _ (refl _)
(subst (λ x → f x ≡ rec (f base) (cong f loop) x) loop (refl _) ≡⟨ subst-in-terms-of-trans-and-cong ⟩
trans (sym (cong f loop))
(trans (refl _) (cong (rec (f base) (cong f loop)) loop)) ≡⟨ cong (trans (sym (cong f loop))) $ trans-reflˡ _ ⟩
trans (sym (cong f loop)) (cong (rec (f base) (cong f loop)) loop) ≡⟨ cong (trans (sym (cong f loop))) rec-loop ⟩
trans (sym (cong f loop)) (cong f loop) ≡⟨ trans-symˡ _ ⟩∎
refl _ ∎)
rec′ : (b : A) → b ≡ b → 𝕊¹ → A
rec′ {A} b ℓ = elim
(const A)
b
(subst (const A) loop b ≡⟨ subst-const _ ⟩
b ≡⟨ ℓ ⟩∎
b ∎)
rec′-loop : cong (rec′ b ℓ) loop ≡ ℓ
rec′-loop = dcong≡→cong≡ elim-loop
𝕊¹≃Susp-Bool : 𝕊¹ ≃ Susp Bool
𝕊¹≃Susp-Bool = Eq.↔→≃ to from to∘from from∘to
where
north≡north =
north ≡⟨ meridian false ⟩
south ≡⟨ sym $ meridian true ⟩∎
north ∎
to : 𝕊¹ → Susp Bool
to = rec north north≡north
from : Susp Bool → 𝕊¹
from = Suspension.rec λ where
.Suspension.northʳ → base
.Suspension.southʳ → base
.Suspension.meridianʳ → if_then refl base else loop
to∘from : ∀ x → to (from x) ≡ x
to∘from = Suspension.elim λ where
.Suspension.northʳ →
to (from north) ≡⟨⟩
north ∎
.Suspension.southʳ →
to (from south) ≡⟨⟩
north ≡⟨ meridian true ⟩∎
south ∎
.Suspension.meridianʳ b →
subst (λ x → to (from x) ≡ x) (meridian b) (refl north) ≡⟨ subst-in-terms-of-trans-and-cong ⟩
trans (sym (cong (to ∘ from) (meridian b)))
(trans (refl _) (cong id (meridian b))) ≡⟨ cong₂ (trans ∘ sym)
(trans (sym $ cong-∘ _ _ _) $
cong (cong to) Suspension.rec-meridian)
(trans (trans-reflˡ _) $
sym $ cong-id _) ⟩
trans (sym (cong to (if b then refl base else loop)))
(meridian b) ≡⟨ lemma b ⟩∎
meridian true ∎
where
lemma : (b : Bool) → _ ≡ _
lemma true =
trans (sym (cong to (if true ⦂ Bool then refl base else loop)))
(meridian true) ≡⟨⟩
trans (sym (cong to (refl base))) (meridian true) ≡⟨ prove (Trans (Sym (Cong _ Refl)) (Lift _)) (Lift _) (refl _) ⟩∎
meridian true ∎
lemma false =
trans (sym (cong to (if false ⦂ Bool then refl base else loop)))
(meridian false) ≡⟨⟩
trans (sym (cong to loop)) (meridian false) ≡⟨ cong (λ p → trans (sym p) (meridian false)) rec-loop ⟩
trans (sym north≡north) (meridian false) ≡⟨ prove (Trans (Sym (Trans (Lift _) (Sym (Lift _)))) (Lift _))
(Trans (Trans (Lift _) (Sym (Lift _))) (Lift _))
(refl _) ⟩
trans (trans (meridian true) (sym $ meridian false))
(meridian false) ≡⟨ trans-[trans-sym]- _ _ ⟩∎
meridian true ∎
from∘to : ∀ x → from (to x) ≡ x
from∘to = elim _
(from (to base) ≡⟨⟩
base ∎)
(subst (λ x → from (to x) ≡ x) loop (refl base) ≡⟨ subst-in-terms-of-trans-and-cong ⟩
trans (sym (cong (from ∘ to) loop))
(trans (refl base) (cong id loop)) ≡⟨ cong₂ (trans ∘ sym)
(trans (sym $ cong-∘ _ to _) $
cong (cong from) rec-loop)
(trans (trans-reflˡ _) $
sym $ cong-id _) ⟩
trans (sym (cong from north≡north)) loop ≡⟨ prove (Trans (Sym (Cong _ (Trans (Lift _) (Sym (Lift _))))) (Lift _))
(Trans (Trans (Cong from (Lift (meridian true)))
(Sym (Cong from (Lift (meridian false)))))
(Lift _))
(refl _) ⟩
trans (trans (cong from (meridian true))
(sym $ cong from (meridian false)))
loop ≡⟨ cong₂ (λ p q → trans (trans p (sym q)) loop)
Suspension.rec-meridian
Suspension.rec-meridian ⟩
trans (trans (if true ⦂ Bool then refl base else loop)
(sym $ if false ⦂ Bool then refl base else loop))
loop ≡⟨⟩
trans (trans (refl base) (sym loop)) loop ≡⟨ trans-[trans-sym]- _ _ ⟩∎
refl base ∎)
𝕊¹≃𝕊¹ : 𝕊¹ ≃ 𝕊 1
𝕊¹≃𝕊¹ =
𝕊¹ ↝⟨ 𝕊¹≃Susp-Bool ⟩
Susp Bool ↔⟨ Suspension.cong-↔ Sphere.Bool↔𝕊⁰ ⟩
Susp (𝕊 0) ↔⟨⟩
𝕊 1 □
trans-commutative : (p q : base ≡ base) → trans p q ≡ trans q p
trans-commutative =
flip $ Transitivity-commutative.commutative base _∙_ ∙-base base-∙
where
_∙_ : 𝕊¹ → 𝕊¹ → 𝕊¹
x ∙ y = rec x (elim (λ x → x ≡ x) loop lemma x) y
where
lemma : subst (λ x → x ≡ x) loop loop ≡ loop
lemma = ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (refl _)
base-∙ : ∀ x → x ∙ base ≡ x
base-∙ _ = refl _
∙-base : ∀ y → base ∙ y ≡ y
∙-base =
elim _ (refl _)
(subst (λ x → rec base loop x ≡ x) loop (refl _) ≡⟨ subst-in-terms-of-trans-and-cong ⟩
trans (sym (cong (rec base loop) loop))
(trans (refl _) (cong id loop)) ≡⟨ cong (trans _) $ trans-reflˡ _ ⟩
trans (sym (cong (rec base loop) loop)) (cong id loop) ≡⟨ cong₂ (trans ∘ sym)
rec-loop
(sym $ cong-id _) ⟩
trans (sym loop) loop ≡⟨ trans-symˡ _ ⟩∎
refl _ ∎)
base≡base≃≡ : {x : 𝕊¹} → (base ≡ base) ≃ (x ≡ x)
base≡base≃≡ = elim
(λ x → (base ≡ base) ≃ (x ≡ x))
Eq.id
(Eq.lift-equality ext $ ⟨ext⟩ λ eq →
_≃_.to (subst (λ x → (base ≡ base) ≃ (x ≡ x)) loop Eq.id) eq ≡⟨ cong (_$ eq) Eq.to-subst ⟩
subst (λ x → base ≡ base → x ≡ x) loop id eq ≡⟨ subst-→ ⟩
subst (λ x → x ≡ x) loop (subst (λ _ → base ≡ base) (sym loop) eq) ≡⟨ cong (subst (λ x → x ≡ x) loop) $ subst-const _ ⟩
subst (λ x → x ≡ x) loop eq ≡⟨ ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (
trans eq loop ≡⟨ trans-commutative _ _ ⟩∎
trans loop eq ∎) ⟩∎
eq ∎)
_
private
module base≡base≃ℤ (univ : Univalence lzero) where
Cover : 𝕊¹ → Type
Cover = rec ℤ (Univ.≃⇒≡ univ Int.successor)
to : base ≡ x → Cover x
to = flip (subst Cover) (+ 0)
≡⇒≃-cong-Cover-loop : Univ.≡⇒≃ (cong Cover loop) ≡ Int.successor
≡⇒≃-cong-Cover-loop =
Univ.≡⇒≃ (cong Cover loop) ≡⟨ cong Univ.≡⇒≃ rec-loop ⟩
Univ.≡⇒≃ (Univ.≃⇒≡ univ Int.successor) ≡⟨ _≃_.right-inverse-of (Univ.≡≃≃ univ) _ ⟩∎
Int.successor ∎
subst-Cover-loop :
∀ i → subst Cover loop i ≡ Int.suc i
subst-Cover-loop i =
subst Cover loop i ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
Univ.≡⇒→ (cong Cover loop) i ≡⟨ cong (λ eq → _≃_.to eq _) ≡⇒≃-cong-Cover-loop ⟩∎
_≃_.to Int.successor i ∎
subst-Cover-sym-loop :
∀ i → subst Cover (sym loop) i ≡ Int.pred i
subst-Cover-sym-loop i =
subst Cover (sym loop) i ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩
_≃_.from (Univ.≡⇒≃ (cong Cover loop)) i ≡⟨ cong (λ eq → _≃_.from eq _) ≡⇒≃-cong-Cover-loop ⟩∎
_≃_.from Int.successor i ∎
module 𝕊¹-G = Groupoid (groupoid 𝕊¹)
loops : ℤ → base ≡ base
loops = loop 𝕊¹-G.^_
to-loops : ∀ i → to (loops i) ≡ i
to-loops (+ zero) =
subst Cover (refl _) (+ 0) ≡⟨ subst-refl _ _ ⟩∎
+ zero ∎
to-loops (+ suc n) =
subst Cover (trans (loops (+ n)) loop) (+ 0) ≡⟨ sym $ subst-subst _ _ _ _ ⟩
subst Cover loop (subst Cover (loops (+ n)) (+ 0)) ≡⟨⟩
subst Cover loop (to (loops (+ n))) ≡⟨ cong (subst Cover loop) $ to-loops (+ n) ⟩
subst Cover loop (+ n) ≡⟨ subst-Cover-loop _ ⟩∎
+ suc n ∎
to-loops -[1+ zero ] =
subst Cover (trans (refl _) (sym loop)) (+ 0) ≡⟨ cong (flip (subst Cover) _) $ trans-reflˡ _ ⟩
subst Cover (sym loop) (+ 0) ≡⟨ subst-Cover-sym-loop _ ⟩∎
-[1+ zero ] ∎
to-loops -[1+ suc n ] =
subst Cover (trans (loops -[1+ n ]) (sym loop)) (+ 0) ≡⟨ sym $ subst-subst _ _ _ _ ⟩
subst Cover (sym loop) (subst Cover (loops -[1+ n ]) (+ 0)) ≡⟨⟩
subst Cover (sym loop) (to (loops -[1+ n ])) ≡⟨ cong (subst Cover (sym loop)) $ to-loops -[1+ n ] ⟩
subst Cover (sym loop) -[1+ n ] ≡⟨ subst-Cover-sym-loop _ ⟩∎
-[1+ suc n ] ∎
loops-pred-loop :
∀ i → trans (loops (Int.pred i)) loop ≡ loops i
loops-pred-loop i =
trans (loops (Int.pred i)) loop ≡⟨ cong (flip trans _ ∘ loops) $ Int.pred≡-1+ i ⟩
trans (loops (Int.-[ 1 ] Int.+ i)) loop ≡⟨ cong (flip trans _) $ sym $ 𝕊¹-G.^∘^ {j = i} Int.-[ 1 ] ⟩
trans (trans (loops i) (loops (Int.-[ 1 ]))) loop ≡⟨⟩
trans (trans (loops i) (trans (refl _) (sym loop))) loop ≡⟨ cong (flip trans _) $ cong (trans _) $ trans-reflˡ _ ⟩
trans (trans (loops i) (sym loop)) loop ≡⟨ trans-[trans-sym]- _ _ ⟩∎
loops i ∎
from : ∀ x → Cover x → base ≡ x
from = elim _
loops
(⟨ext⟩ λ i →
subst (λ x → Cover x → base ≡ x) loop loops i ≡⟨ subst-→ ⟩
subst (base ≡_) loop (loops (subst Cover (sym loop) i)) ≡⟨ sym trans-subst ⟩
trans (loops (subst Cover (sym loop) i)) loop ≡⟨ cong (flip trans _ ∘ loops) $ subst-Cover-sym-loop _ ⟩
trans (loops (Int.pred i)) loop ≡⟨ loops-pred-loop i ⟩∎
loops i ∎)
from-to : (eq : base ≡ x) → from x (to eq) ≡ eq
from-to = elim¹
(λ {x} eq → from x (to eq) ≡ eq)
(from base (to (refl base)) ≡⟨⟩
loops (subst Cover (refl base) (+ 0)) ≡⟨ cong loops $ subst-refl _ _ ⟩
loops (+ 0) ≡⟨⟩
refl base ∎)
loops-+ : ∀ i j → loops (i Int.+ j) ≡ trans (loops i) (loops j)
loops-+ i j =
loops (i Int.+ j) ≡⟨ cong loops $ Int.+-comm i ⟩
loops (j Int.+ i) ≡⟨ sym $ 𝕊¹-G.^∘^ j ⟩∎
trans (loops i) (loops j) ∎
base≡base≃ℤ :
Univalence lzero →
(base ≡ base) ≃ ℤ
base≡base≃ℤ univ = Eq.↔→≃ to loops to-loops from-to
where
open base≡base≃ℤ univ
Fundamental-group≃ℤ :
Univalence lzero →
Fundamental-group (𝕊¹ , base) ≃ᴳ ℤ-group
Fundamental-group≃ℤ univ = G.≃ᴳ-sym λ where
.G.Homomorphic.related → inverse
(∥ base ≡ base ∥[1+ 1 ] ↝⟨ T.∥∥-cong $ base≡base≃ℤ univ ⟩
∥ ℤ ∥[1+ 1 ] ↔⟨ _⇔_.to (T.+⇔∥∥↔ {n = 1}) Int.ℤ-set ⟩□
ℤ □)
.G.Homomorphic.homomorphic i j → cong T.∣_∣ (loops-+ i j)
where
open base≡base≃ℤ univ
𝕊¹-groupoid :
Univalence lzero →
H-level 3 𝕊¹
𝕊¹-groupoid univ {x} {y} =
$⟨ (λ {_ _} → Int.ℤ-set) ⟩
Is-set ℤ ↝⟨ H-level-cong _ 2 (inverse $ base≡base≃ℤ univ) ⦂ (_ → _) ⟩
Is-set (base ≡ base) ↝⟨ (λ s →
elim
(λ x → ∀ y → Is-set (x ≡ y))
(elim _ s (H-level-propositional ext 2 _ _))
((Π-closure ext 1 λ _ →
H-level-propositional ext 2)
_ _)
x y) ⟩□
Is-set (x ≡ y) □
𝕊¹→𝕊¹≃Σ𝕊¹≡ : (𝕊¹ → 𝕊¹) ≃ ∃ λ (x : 𝕊¹) → x ≡ x
𝕊¹→𝕊¹≃Σ𝕊¹≡ = Eq.↔→≃ to from to-from from-to
where
to : (𝕊¹ → 𝕊¹) → ∃ λ (x : 𝕊¹) → x ≡ x
to f = f base , cong f loop
from : (∃ λ (x : 𝕊¹) → x ≡ x) → (𝕊¹ → 𝕊¹)
from = uncurry rec
to-from : ∀ p → to (from p) ≡ p
to-from (x , eq) = cong (x ,_)
(cong (rec x eq) loop ≡⟨ rec-loop ⟩∎
eq ∎)
from-to : ∀ f → from (to f) ≡ f
from-to f =
rec (f base) (cong f loop) ≡⟨ sym η-rec ⟩∎
f ∎
𝕊¹→𝕊¹≃𝕊¹×ℤ :
Univalence lzero →
(𝕊¹ → 𝕊¹) ≃ (𝕊¹ × ℤ)
𝕊¹→𝕊¹≃𝕊¹×ℤ univ =
(𝕊¹ → 𝕊¹) ↝⟨ 𝕊¹→𝕊¹≃Σ𝕊¹≡ ⟩
(∃ λ (x : 𝕊¹) → x ≡ x) ↝⟨ (∃-cong λ _ → inverse base≡base≃≡) ⟩
𝕊¹ × base ≡ base ↝⟨ (∃-cong λ _ → base≡base≃ℤ univ) ⟩□
𝕊¹ × ℤ □
𝕊¹→𝕊¹≃𝕊¹×ℤ-id :
(univ : Univalence lzero) →
_≃_.to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ) id ≡ (base , + 1)
𝕊¹→𝕊¹≃𝕊¹×ℤ-id univ = _≃_.from-to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ)
(rec base (trans (refl base) loop) ≡⟨ cong (rec base) $ trans-reflˡ _ ⟩
rec base loop ≡⟨ cong (rec base) $ cong-id _ ⟩
rec base (cong id loop) ≡⟨ sym η-rec ⟩∎
id ∎)
𝕊¹→𝕊¹≃𝕊¹×ℤ-const :
(univ : Univalence lzero) →
_≃_.to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ) (const base) ≡ (base , + 0)
𝕊¹→𝕊¹≃𝕊¹×ℤ-const univ = _≃_.from-to (𝕊¹→𝕊¹≃𝕊¹×ℤ univ)
(rec base (refl base) ≡⟨ cong (rec base) $ sym $ cong-const _ ⟩
rec base (cong (const base) loop) ≡⟨ sym η-rec ⟩∎
const base ∎)
∥⊤∥¹≃𝕊¹ : ∥ ⊤ ∥¹ ≃ 𝕊¹
∥⊤∥¹≃𝕊¹ = _↔_.from ≃↔≃ $ PE.↔→≃
(O.recᴾ λ where
.O.∣∣ʳ _ → base
.O.∣∣-constantʳ _ _ → loopᴾ)
(recᴾ O.∣ _ ∣ (O.∣∣-constantᴾ _ _))
(elimᴾ _ P.refl (λ _ → P.refl))
(O.elimᴾ λ where
.O.∣∣ʳ _ → P.refl
.O.∣∣-constantʳ _ _ _ → P.refl)
loop≢refl : loop ≢ refl base
loop≢refl =
E.Stable-¬
E.[ loop ≡ refl base →⟨ Type-set ⟩
Is-set Type →⟨ Univ.¬-Type-set univ ⟩□
⊥ □
]
where
module _ (loop≡refl : loop ≡ refl base) where
refl≡ : (A : Type) (A≡A : A ≡ A) → refl A ≡ A≡A
refl≡ A A≡A =
refl A ≡⟨⟩
refl (rec A A≡A base) ≡⟨ sym $ cong-refl _ ⟩
cong (rec A A≡A) (refl base) ≡⟨ cong (cong (rec A A≡A)) $ sym loop≡refl ⟩
cong (rec A A≡A) loop ≡⟨ rec-loop ⟩∎
A≡A ∎
Type-set : Is-set Type
Type-set {x = A} {y = B} =
elim¹ (λ p → ∀ q → p ≡ q)
(refl≡ A)
¬-𝕊¹-set : ¬ Is-set 𝕊¹
¬-𝕊¹-set =
Is-set 𝕊¹ ↝⟨ (λ h → h) ⟩
Is-proposition (base ≡ base) ↝⟨ (λ h → h _ _) ⟩
loop ≡ refl base ↝⟨ loop≢refl ⟩□
⊥ □
¬-Is-proposition-∥∥¹ :
¬ ({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹)
¬-Is-proposition-∥∥¹ {a} =
({A : Type a} → Is-proposition A → Is-proposition ∥ A ∥¹) ↝⟨ _$ H-level.mono₁ 0 (↑-closure 0 ⊤-contractible) ⟩
Is-proposition ∥ ↑ a ⊤ ∥¹ ↝⟨ H-level-cong _ 1 (O.∥∥¹-cong-↔ Bijection.↑↔) ⟩
Is-proposition ∥ ⊤ ∥¹ ↝⟨ H-level-cong _ 1 ∥⊤∥¹≃𝕊¹ ⟩
Is-proposition 𝕊¹ ↝⟨ ¬-𝕊¹-set ∘ H-level.mono₁ 1 ⟩□
⊥ □
not-refl : (x : 𝕊¹) → x ≡ x
not-refl = elim _
loop
(subst (λ z → z ≡ z) loop loop ≡⟨ ≡⇒↝ _ (sym [subst≡]≡[trans≡trans]) (refl _) ⟩∎
loop ∎)
not-refl≢refl : not-refl ≢ refl
not-refl≢refl =
not-refl ≡ refl ↝⟨ cong (_$ _) ⟩
loop ≡ refl base ↝⟨ loop≢refl ⟩□
⊥ □
∃≢refl : ∃ λ (f : (x : 𝕊¹) → x ≡ x) → f ≢ refl
∃≢refl = not-refl , not-refl≢refl
¬-type-of-refl-propositional :
∃ λ (A : Type a) → ¬ Is-proposition ((x : A) → x ≡ x)
¬-type-of-refl-propositional {a} =
↑ _ 𝕊¹
, (Is-proposition (∀ x → x ≡ x) ↝⟨ (λ prop → prop _ _) ⟩
cong lift ∘ proj₁ ∃≢refl ∘ lower ≡ cong lift ∘ refl ∘ lower ↝⟨ cong (_∘ lift) ⟩
cong lift ∘ proj₁ ∃≢refl ≡ cong lift ∘ refl ↝⟨ cong (cong lower ∘_) ⟩
cong lower ∘ cong lift ∘ proj₁ ∃≢refl ≡
cong lower ∘ cong lift ∘ refl ↝⟨ ≡⇒↝ _ (cong₂ _≡_ (⟨ext⟩ λ _ → cong-∘ _ _ _) (⟨ext⟩ λ _ → cong-∘ _ _ _)) ⟩
cong id ∘ proj₁ ∃≢refl ≡ cong id ∘ refl ↝⟨ ≡⇒↝ _ (sym $ cong₂ _≡_ (⟨ext⟩ λ _ → cong-id _) (⟨ext⟩ λ _ → cong-id _)) ⟩
proj₁ ∃≢refl ≡ refl ↝⟨ proj₂ ∃≢refl ⟩□
⊥ □)
all-points-on-the-circle-are-merely-equal :
(x : 𝕊¹) → ∥ x ≡ base ∥
all-points-on-the-circle-are-merely-equal =
elim _
∣ refl base ∣
(Trunc.truncation-is-proposition _ _)
all-points-on-the-circle-are-¬¬-equal :
(x : 𝕊¹) → ¬ ¬ x ≡ base
all-points-on-the-circle-are-¬¬-equal x =
x ≢ base ↝⟨ Trunc.rec ⊥-propositional ⟩
¬ ∥ x ≡ base ∥ ↝⟨ _$ all-points-on-the-circle-are-merely-equal x ⟩□
⊥ □
¬-all-points-on-the-circle-are-equal :
¬ ((x : 𝕊¹) → x ≡ base)
¬-all-points-on-the-circle-are-equal =
((x : 𝕊¹) → x ≡ base) ↝⟨ (λ hyp x y → x ≡⟨ hyp x ⟩
base ≡⟨ sym (hyp y) ⟩∎
y ∎) ⟩
Is-proposition 𝕊¹ ↝⟨ mono₁ 1 ⟩
Is-set 𝕊¹ ↝⟨ ¬-𝕊¹-set ⟩□
⊥ □
¬-double-negation-shift :
¬ ({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))
¬-double-negation-shift =
({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x)) ↝⟨ _$ all-points-on-the-circle-are-¬¬-equal ⟩
¬ ¬ ((x : 𝕊¹) → x ≡ base) ↝⟨ _$ ¬-all-points-on-the-circle-are-equal ⟩□
⊥ □
¬-¬¬-modality-Has-choice-for-𝕊¹ :
¬ Modality.Has-choice-for (¬¬-modality ext) 𝕊¹
¬-¬¬-modality-Has-choice-for-𝕊¹ =
Has-choice-for 𝕊¹ →⟨ (λ hyp → hyp .proj₁) ⟩
({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬¬ P x) → ¬¬ ((x : 𝕊¹) → P x)) →⟨ implicit-∀-cong _ $ →-cong-→ (∀-cong _ λ _ → DN.wrap) DN.run ⟩
({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x)) →⟨ ¬-double-negation-shift ⟩□
⊥ □
where
open Modality (¬¬-modality ext)
¬-excluded-middle : ¬ ({A : Type} → Dec A)
¬-excluded-middle =
({A : Type} → Dec A) ↝⟨ (λ em ¬¬a → [ id , ⊥-elim ∘ ¬¬a ] em) ⟩
({A : Type} → ¬ ¬ A → A) ↝⟨ (λ dne → flip _$_ ∘ (dne ∘_)) ⟩
({P : 𝕊¹ → Type} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x)) ↝⟨ ¬-double-negation-shift ⟩□
⊥ □
¬-generalised-proj₁-closure :
¬ ({A : Type} {B : A → Type} →
(∀ a → ∥ B a ∥) →
∀ n → H-level n (Σ A B) → H-level n A)
¬-generalised-proj₁-closure generalised-proj₁-closure =
$⟨ singleton-contractible _ ⟩
Contractible (Σ 𝕊¹ (_≡ base)) ↝⟨ generalised-proj₁-closure
all-points-on-the-circle-are-merely-equal
0 ⟩
Contractible 𝕊¹ ↝⟨ mono (zero≤ 2) ⟩
Is-set 𝕊¹ ↝⟨ ¬-𝕊¹-set ⟩□
⊥ □
𝕊¹≄ᴮ𝕊¹×𝕊¹ : ¬ (𝕊¹ , base) ≃ᴮ ((𝕊¹ , base) PT.× (𝕊¹ , base))
𝕊¹≄ᴮ𝕊¹×𝕊¹ =
E.Stable-¬
E.[ (𝕊¹ , base) ≃ᴮ ((𝕊¹ , base) PT.× (𝕊¹ , base)) ↝⟨ ≃ᴮ→≃ᴳ (𝕊¹ , base) ((𝕊¹ , base) PT.× (𝕊¹ , base)) 0 ⟩
Fundamental-group (𝕊¹ , base) ≃ᴳ
Fundamental-group ((𝕊¹ , base) PT.× (𝕊¹ , base)) ↝⟨ flip G.↝ᴳ-trans (Homotopy-group-[1+ 0 ]-× (𝕊¹ , base) (𝕊¹ , base)) ⟩
Fundamental-group (𝕊¹ , base) ≃ᴳ
(Fundamental-group (𝕊¹ , base) G.× Fundamental-group (𝕊¹ , base)) ↝⟨ flip G.↝ᴳ-trans
(G.↝-× (Fundamental-group≃ℤ univ) (Fundamental-group≃ℤ univ)) ∘
G.↝ᴳ-trans (G.≃ᴳ-sym (Fundamental-group≃ℤ univ)) ⟩
ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group) ↝⟨ C.ℤ≄ᴳℤ×ℤ ⟩□
⊥ □
]
𝕊¹≄𝕊¹×𝕊¹ : ¬ 𝕊¹ ≃ (𝕊¹ × 𝕊¹)
𝕊¹≄𝕊¹×𝕊¹ hyp =
let x , y = _≃_.to hyp base in
all-points-on-the-circle-are-¬¬-equal x λ x≡base →
all-points-on-the-circle-are-¬¬-equal y λ y≡base →
𝕊¹≄ᴮ𝕊¹×𝕊¹ (hyp , cong₂ _,_ x≡base y≡base)
Circle :
∀ {e⁺} →
(∀ {a p} → P.Equality-with-paths a p e⁺) →
(p : Level) → Type (lsuc p)
Circle eq p =
∃ λ (𝕊¹ : Type) →
∃ λ (base : 𝕊¹) →
∃ λ (loop : base ≡.≡ base) →
(P : 𝕊¹ → Type p)
(b : P base)
(ℓ : ≡.subst P loop b ≡.≡ b) →
∃ λ (elim : (x : 𝕊¹) → P x) →
∃ λ (elim-base : elim base ≡.≡ b) →
≡.subst (λ b → ≡.subst P loop b ≡.≡ b)
elim-base
(≡.dcong elim loop)
≡.≡
ℓ
where
module ≡ = P.Derived-definitions-and-properties eq
Circle≃Circle : Circle P.equality-with-paths p ≃ Circle eq p
Circle≃Circle =
∃-cong λ _ →
∃-cong λ _ →
Σ-cong (inverse ≡↔≡) λ loop →
∀-cong ext λ P →
∀-cong ext λ b →
Π-cong-contra ext subst≡↔subst≡ λ ℓ →
∃-cong λ f →
Σ-cong (inverse ≡↔≡) λ f-base →
let lemma = P.elim¹
(λ eq → _↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
eq
(P.dcong f loop)) ≡
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
eq
(_↔_.from subst≡↔subst≡ (P.dcong f loop)))
(_↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
P.refl
(P.dcong f loop)) ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $
P.subst-refl (λ b → P.subst P loop b P.≡ b) _ ⟩
_↔_.from subst≡↔subst≡ (P.dcong f loop) ≡⟨ sym $ _↔_.from ≡↔≡ $
P.subst-refl (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) _ ⟩∎
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
P.refl
(_↔_.from subst≡↔subst≡ (P.dcong f loop)) ∎)
_
in
P.subst
(λ b → P.subst P loop b P.≡ b)
f-base
(P.dcong f loop) P.≡
_↔_.to subst≡↔subst≡ ℓ ↔⟨ ≡↔≡ F.∘ inverse (from≡↔≡to (Eq.↔⇒≃ subst≡↔subst≡)) F.∘ inverse ≡↔≡ ⟩
_↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
f-base
(P.dcong f loop)) P.≡
ℓ ↝⟨ ≡⇒↝ _ (cong (P._≡ _) lemma) ⟩
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
f-base
(_↔_.from subst≡↔subst≡ (P.dcong f loop)) P.≡
ℓ ↝⟨ ≡⇒↝ _ $ cong (λ eq → P.subst (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) f-base eq P.≡ ℓ) $
_↔_.from-to (inverse subst≡↔subst≡) dcong≡dcong ⟩
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
f-base
(dcong f (_↔_.from ≡↔≡ loop)) P.≡
ℓ ↔⟨ inverse subst≡↔subst≡ ⟩□
subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
(_↔_.from ≡↔≡ f-base)
(dcong f (_↔_.from ≡↔≡ loop)) ≡
ℓ □
circleᴾ : Circle P.equality-with-paths p
circleᴾ =
𝕊¹
, base
, loopᴾ
, λ P b ℓ →
let elim = elimᴾ P b (PI.subst≡→[]≡ {B = P} ℓ)
in
elim
, P.refl
, (P.subst (λ b → P.subst P loopᴾ b P.≡ b) P.refl
(P.dcong elim loopᴾ) P.≡⟨ P.subst-refl (λ b → P.subst P loopᴾ b P.≡ b) _ ⟩
P.dcong elim loopᴾ P.≡⟨ PI.dcong-subst≡→[]≡ {f = elim} {eq₂ = ℓ} P.refl ⟩∎
ℓ ∎)
circle : Circle eq p
circle = _≃_.to Circle≃Circle circleᴾ
_ :
let _ , base′ , _ , elim′ = circle {p = p} in
∀ {P b ℓ} →
proj₁ (elim′ P b ℓ) base′ ≡ b
_ = refl _
elim-loop-circle :
let _ , _ , loop′ , elim′ = circle {p = p} in
∀ {P b ℓ} →
dcong (proj₁ (elim′ P b ℓ)) loop′ ≡ ℓ
elim-loop-circle {P} {b} {ℓ} =
let _ , _ , loop′ , elim′ = circle
elim″ , elim″-base , elim″-loop = elim′ P b ℓ
lemma =
refl _ ≡⟨ sym from-≡↔≡-refl ⟩
_↔_.from ≡↔≡ P.refl ≡⟨ refl _ ⟩∎
elim″-base ∎
in
dcong elim″ loop′ ≡⟨ sym $ subst-refl _ _ ⟩
subst (λ b → subst P loop′ b ≡ b) (refl _) (dcong elim″ loop′) ≡⟨ cong (λ eq → subst (λ b → subst P loop′ b ≡ b) eq (dcong elim″ loop′)) lemma ⟩
subst (λ b → subst P loop′ b ≡ b) elim″-base (dcong elim″ loop′) ≡⟨ elim″-loop ⟩∎
ℓ ∎
Circle≃Circle′ : Circle P.equality-with-paths p ≃ Circle eq p
Circle≃Circle′ =
∃-cong λ _ →
∃-cong λ _ →
Σ-cong (inverse ≡↔≡) λ loop →
∀-cong ext λ P →
∀-cong ext λ b →
Π-cong ext (inverse subst≡↔subst≡) λ ℓ →
∃-cong λ f →
Σ-cong (inverse ≡↔≡) λ f-base →
let lemma = P.elim¹
(λ eq → _↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
eq
(P.dcong f loop)) ≡
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
eq
(_↔_.from subst≡↔subst≡ (P.dcong f loop)))
(_↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
P.refl
(P.dcong f loop)) ≡⟨ cong (_↔_.from subst≡↔subst≡) $ _↔_.from ≡↔≡ $
P.subst-refl (λ b → P.subst P loop b P.≡ b) _ ⟩
_↔_.from subst≡↔subst≡ (P.dcong f loop) ≡⟨ sym $ _↔_.from ≡↔≡ $
P.subst-refl (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) _ ⟩∎
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
P.refl
(_↔_.from subst≡↔subst≡ (P.dcong f loop)) ∎)
_
in
P.subst
(λ b → P.subst P loop b P.≡ b)
f-base
(P.dcong f loop) P.≡
ℓ ↔⟨ ≡↔≡ F.∘ from-isomorphism (inverse $ Eq.≃-≡ $ Eq.↔⇒≃ $ inverse subst≡↔subst≡) F.∘ inverse ≡↔≡ ⟩
_↔_.from subst≡↔subst≡
(P.subst
(λ b → P.subst P loop b P.≡ b)
f-base
(P.dcong f loop)) P.≡
_↔_.from subst≡↔subst≡ ℓ ↝⟨ ≡⇒↝ _ (cong (P._≡ _↔_.from subst≡↔subst≡ ℓ) lemma) ⟩
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
f-base
(_↔_.from subst≡↔subst≡ (P.dcong f loop)) P.≡
_↔_.from subst≡↔subst≡ ℓ ↝⟨ ≡⇒↝ _ $ cong (λ eq → P.subst (λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b) f-base eq P.≡ _↔_.from subst≡↔subst≡ ℓ) $
_↔_.from-to (inverse subst≡↔subst≡) dcong≡dcong ⟩
P.subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
f-base
(dcong f (_↔_.from ≡↔≡ loop)) P.≡
_↔_.from subst≡↔subst≡ ℓ ↔⟨ inverse subst≡↔subst≡ ⟩□
subst
(λ b → subst P (_↔_.from ≡↔≡ loop) b ≡ b)
(_↔_.from ≡↔≡ f-base)
(dcong f (_↔_.from ≡↔≡ loop)) ≡
_↔_.from subst≡↔subst≡ ℓ □
circle′ : Circle eq p
circle′ = _≃_.to Circle≃Circle′ circleᴾ