{-# OPTIONS --without-K #-}
open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import Sec2preliminaries
module Sec3hedberg where
discr→pathColl : {X : Type} → has-dec-eq X → pathColl X
discr→pathColl dec x₁ x₂ with (dec x₁ x₂)
discr→pathColl dec x₁ x₂ | inl p = (λ _ → p) , (λ _ _ → idp)
discr→pathColl dec x₁ x₂ | inr np = idf _ , λ p → Empty-elim (np p)
pathColl→isSet : {X : Type} → pathColl X → is-set X
pathColl→isSet {X} pc x₁ x₂ = all-paths-is-prop paths-equal where
claim : (y₁ y₂ : X) → (p : y₁ == y₂) → p == ! (fst (pc _ _) idp) ∙ fst (pc _ _) p
claim x₁ .x₁ idp = ! (!-inv-l (fst (pc x₁ x₁) idp))
paths-equal : (p₁ p₂ : x₁ == x₂) → p₁ == p₂
paths-equal p₁ p₂ =
p₁ =⟨ claim _ _ p₁ ⟩
! (fst (pc _ _) idp) ∙ fst (pc _ _) p₁ =⟨ ap (λ q → (! (fst (pc x₁ x₁) idp)) ∙ q) (snd (pc _ _) p₁ p₂) ⟩
! (fst (pc _ _) idp) ∙ fst (pc _ _) p₂ =⟨ ! (claim _ _ p₂) ⟩
p₂ ∎
hedberg : {X : Type} → has-dec-eq X → is-set X
hedberg = pathColl→isSet ∘ discr→pathColl
stable : Type → Type
stable X = ¬ (¬ X) → X
separated : Type → Type
separated X = (x₁ x₂ : X) → stable (x₁ == x₂)
sep→set : {X : Type} → (separated X) → ({x₁ x₂ : X} → Funext {¬ (x₁ == x₂)} {Empty}) → is-set X
sep→set {X} sep ⊥-funext = pathColl→isSet isPc where
isPc : pathColl X
isPc x₁ x₂ = f , c where
f : x₁ == x₂ → x₁ == x₂
f = (sep x₁ x₂) ∘ (λ p np → np p)
c : const f
c p₁ p₂ =
f p₁ =⟨ idp ⟩
(sep x₁ x₂) (λ np → np p₁) =⟨ ap (sep x₁ x₂)
(⊥-funext _ _ λ np → Empty-elim {A = λ _ → np p₁ == np p₂} (np p₁)) ⟩
(sep x₁ x₂) (λ np → np p₂) =⟨ idp ⟩
f p₂ ∎
postulate
Trunc : Type → Type
h-tr : (X : Type) → is-prop (Trunc X)
∣_∣ : {X : Type} → X → Trunc X
rec : {X : Type} → {P : Type} → (is-prop P) → (X → P) → Trunc X → P
trunc-β : {X : Type} → {P : Type} → (pp : is-prop P) → (f : X → P) → (x : X) → rec pp f ∣ x ∣ == f x
trunc-β pp f x = prop-has-all-paths pp _ _
module _ (X : Type) (P : Trunc X → Type) (h : (z : Trunc X) → is-prop (P z)) (k : (x : X) → P(∣ x ∣)) where
total : Type
total = Σ (Trunc X) P
j : X → total
j x = ∣ x ∣ , k x
total-prop : is-prop total
total-prop = Σ-level (h-tr X) h
total-map : Trunc X → total
total-map = rec total-prop j
induction : (z : Trunc X) → P z
induction z = transport P (prop-has-all-paths (h-tr _) _ _) (snd (total-map z))
trunc-functorial : {X Y : Type} → (X → Y) → (Trunc X → Trunc Y)
trunc-functorial {X} {Y} f = rec (h-tr Y) (∣_∣ ∘ f)
impred : {X : Type} → (Trunc X ↔₀₁ ((P : Type) → (is-prop P) → (X → P) → P))
impred {X} = one , two where
one : Trunc X → (P : Type) → (is-prop P) → (X → P) → P
one z P p-prop f = rec p-prop f z
two : ((P : Type) → (is-prop P) → (X → P) → P) → Trunc X
two k = k (Trunc X) (h-tr _) ∣_∣
hstable : Type → Type
hstable X = Trunc X → X
hseparated : Type → Type
hseparated X = (x₁ x₂ : X) → hstable (x₁ == x₂)
set-characterizations : {X : Type} → (pathColl X → is-set X)
× ((is-set X → hseparated X)
× (hseparated X → pathColl X))
set-characterizations {X} = one , two , three where
one : pathColl X → is-set X
one = pathColl→isSet
two : is-set X → hseparated X
two h = λ x₁ x₂ → rec (h x₁ x₂) (idf _)
three : hseparated X → pathColl X
three hsep x₁ x₂ = f , c where
f = (hsep _ _) ∘ ∣_∣
c = λ p₁ p₂ → f p₁ =⟨ idp ⟩
hsep _ _ (∣ p₁ ∣) =⟨ ap (hsep _ _) (prop-has-all-paths (h-tr _) _ _) ⟩
hsep _ _ (∣ p₂ ∣) =⟨ idp ⟩
f p₂ ∎
pathColl→isSet-local : {X : Type} → {x₀ : X} → ((y : X) → coll (x₀ == y)) → (y : X) → is-prop (x₀ == y)
pathColl→isSet-local {X} {x₀} pc y = all-paths-is-prop paths-equal where
claim : (y : X) → (p : x₀ == y) → p == ! (fst (pc _) idp) ∙ fst (pc _) p
claim .x₀ idp = ! (!-inv-l (fst (pc _) idp))
paths-equal : (p₁ p₂ : x₀ == y) → p₁ == p₂
paths-equal p₁ p₂ =
p₁ =⟨ claim _ p₁ ⟩
! (fst (pc _) idp) ∙ fst (pc _) p₁ =⟨ ap (λ q → (! (fst (pc x₀) idp)) ∙ q) (snd (pc y) p₁ p₂) ⟩
! (fst (pc _) idp) ∙ fst (pc _) p₂ =⟨ ! (claim _ p₂) ⟩
p₂ ∎
hedberg-local : {X : Type} → {x₀ : X} → ((y : X) → (x₀ == y) + ¬(x₀ == y)) → (y : X) → is-prop (x₀ == y)
hedberg-local {X} {x₀} dec = pathColl→isSet-local local-pathColl where
local-pathColl : (y : X) → coll (x₀ == y)
local-pathColl y with (dec y)
local-pathColl y₁ | inl p = (λ _ → p) , (λ _ _ → idp)
local-pathColl y₁ | inr np = idf _ , (λ p → Empty-elim (np p))
sep→set-local : {X : Type} → {x₀ : X} → ((y : X) → stable (x₀ == y)) → ({y : X} → Funext {¬ (x₀ == y)} {Empty}) → (y : X) → is-prop (x₀ == y)
sep→set-local {X} {x₀} sep ⊥-funext = pathColl→isSet-local is-pathColl where
is-pathColl : (y : X) → coll (x₀ == y)
is-pathColl y = f , c where
f : x₀ == y → x₀ == y
f = (sep y) ∘ (λ p np → np p)
c : const f
c p₁ p₂ =
f p₁ =⟨ idp ⟩
(sep _) (λ np → np p₁) =⟨ ap (sep _)
(⊥-funext _ _ λ np → Empty-elim {A = λ _ → np p₁ == np p₂} (np p₁)) ⟩
(sep _) (λ np → np p₂) =⟨ idp ⟩
f p₂ ∎
set-characterizations-local : {X : Type} → {x₀ : X} →
(((y : X) → coll (x₀ == y)) → (y : X) → is-prop (x₀ == y))
× ((((y : X) → is-prop (x₀ == y)) → (y : X) → hstable (x₀ == y))
× (((y : X) → hstable (x₀ == y)) → (y : X) → coll (x₀ == y)))
set-characterizations-local {X} {x₀} = one , two , three where
one = pathColl→isSet-local
two : ((y : X) → is-prop (x₀ == y)) → (y : X) → hstable (x₀ == y)
two h y = rec (h y) (idf _)
three : ((y : X) → hstable (x₀ == y)) → (y : X) → coll (x₀ == y)
three hsep y = f , c where
f = (hsep _) ∘ ∣_∣
c = λ p₁ p₂ →
f p₁ =⟨ idp ⟩
(hsep _) ∣ p₁ ∣ =⟨ ap (hsep _) (prop-has-all-paths (h-tr _) _ _) ⟩
(hsep _) ∣ p₂ ∣ =⟨ idp ⟩
f p₂ ∎