{-# OPTIONS --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 Prelude
open import Bijection equality-with-J as Bijection using (_↔_)
import Bijection P.equality-with-J as PB
open import Equality.Path.Isomorphisms eq
import Equality.Path.Isomorphisms P.equality-with-paths as PI
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as Trunc
using (∥_∥; ∣_∣)
open import Nat equality-with-J
open import Univalence-axiom equality-with-J using (¬-Set-set)
private
variable
a p : Level
A : Set p
P : A → Set p
b ℓ : A
data 𝕊¹ : Set where
base : 𝕊¹
loopᴾ : base P.≡ base
loop : base ≡ base
loop = _↔_.from ≡↔≡ loopᴾ
elimᴾ :
(P : 𝕊¹ → Set 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 : 𝕊¹ → Set 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 _)
rec : (b : A) → b ≡ b → 𝕊¹ → A
rec b ℓ = recᴾ b (_↔_.to ≡↔≡ ℓ)
rec-loop : cong (rec b ℓ) loop ≡ ℓ
rec-loop = cong-≡↔≡ (refl _)
rec′ : (b : A) → b ≡ b → 𝕊¹ → A
rec′ {A = 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
loop≢refl : loop ≢ refl base
loop≢refl loop≡refl = ¬-Set-set univ Set-set
where
refl≡ : (A : Set) (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 ∎
Set-set : Is-set Set
Set-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 ⟩□
⊥ □
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 : Set a) → ¬ Is-proposition ((x : A) → x ≡ x)
¬-type-of-refl-propositional {a = 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 : 𝕊¹ → Set} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x))
¬-double-negation-shift =
({P : 𝕊¹ → Set} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x)) ↝⟨ _$ all-points-on-the-circle-are-¬¬-equal ⟩
¬ ¬ ((x : 𝕊¹) → x ≡ base) ↝⟨ _$ ¬-all-points-on-the-circle-are-equal ⟩□
⊥ □
¬-excluded-middle : ¬ ({A : Set} → Dec A)
¬-excluded-middle =
({A : Set} → Dec A) ↝⟨ (λ em ¬¬a → [ id , ⊥-elim ∘ ¬¬a ] em) ⟩
({A : Set} → ¬ ¬ A → A) ↝⟨ (λ dne → flip _$_ ∘ (dne ∘_)) ⟩
({P : 𝕊¹ → Set} → ((x : 𝕊¹) → ¬ ¬ P x) → ¬ ¬ ((x : 𝕊¹) → P x)) ↝⟨ ¬-double-negation-shift ⟩□
⊥ □
¬-generalised-proj₁-closure :
¬ ({A : Set} {B : A → Set} →
(∀ 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 ⟩□
⊥ □
Circle :
∀ {e⁺} →
(∀ {a p} → P.Equality-with-paths a p e⁺) →
(p : Level) → Set (lsuc p)
Circle eq p =
∃ λ (𝕊¹ : Set) →
∃ λ (base : 𝕊¹) →
∃ λ (loop : base E.≡ base) →
(P : 𝕊¹ → Set p)
(b : P base)
(ℓ : E.subst P loop b E.≡ b) →
∃ λ (elim : (x : 𝕊¹) → P x) →
∃ λ (elim-base : elim base E.≡ b) →
E.subst (λ b → E.subst P loop b E.≡ b)
elim-base
(E.dcong elim loop)
E.≡
ℓ
where
module E = 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} 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 = P} {b = b} {ℓ = ℓ} =
let _ , _ , loop′ , elim′ = circle
elim″ , elim″-base , elim″-loop = elim′ P b ℓ
lemma =
refl _ ≡⟨ sym from-≡↔≡-refl ⟩
_↔_.from ≡↔≡ P.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ᴾ