Martin Escardo

UF things that depend on non-UF things.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-Miscelanea where

open import SpartanMLTT

open import Plus-Properties
open import UF-Base
open import UF-Subsingletons
open import UF-FunExt
open import UF-Subsingletons-FunExt
open import UF-Retracts

decidable-is-collapsible : {X : π€ Μ } β decidable X β collapsible X
decidable-is-collapsible (inl x) = pointed-types-are-collapsible x
decidable-is-collapsible (inr u) = empty-types-are-collapsible u

open import DiscreteAndSeparated

discrete-is-Id-collapsible : {X : π€ Μ } β is-discrete X β Id-collapsible X
discrete-is-Id-collapsible d = decidable-is-collapsible (d _ _)

discrete-types-are-sets : {X : π€ Μ } β is-discrete X β is-set X
discrete-types-are-sets d = Id-collapsibles-are-sets(discrete-is-Id-collapsible d)

isolated-is-h-isolated : {X : π€ Μ } (x : X) β is-isolated x β is-h-isolated x
isolated-is-h-isolated {π€} {X} x i {y} = local-hedberg x (Ξ» y β Ξ³ y (i y)) y
where
Ξ³ : (y : X) β decidable (x β‘ y) β Ξ£ \(f : x β‘ y β x β‘ y) β constant f
Ξ³ y (inl p) = (Ξ» _ β p) , (Ξ» q r β refl)
Ξ³ y (inr n) = id , (Ξ» q r β π-elim (n r))

isolated-inl : {X : π€ Μ } (x : X) (i : is-isolated x) (y : X) (r : x β‘ y) β i y β‘ inl r
isolated-inl x i y r =
equality-cases (i y)
(Ξ» (p : x β‘ y) (q : i y β‘ inl p) β q β ap inl (isolated-is-h-isolated x i p r))
(Ξ» (h : Β¬(x β‘ y)) (q : i y β‘ inr h) β π-elim(h r))

discrete-inl : {X : π€ Μ } (d : is-discrete X) (x y : X) (r : x β‘ y) β d x y β‘ inl r
discrete-inl d x y r =
equality-cases (d x y)
(Ξ» (p : x β‘ y) (q : d x y β‘ inl p) β q β ap inl (discrete-types-are-sets d p r))
(Ξ» (h : Β¬(x β‘ y)) (q : d x y β‘ inr h) β π-elim(h r))

discrete-inr : {X : π€ Μ } β funext π€ π€β
β (d : is-discrete X) (x y : X) (n : Β¬(x β‘ y)) β d x y β‘ inr n
discrete-inr fe d x y n =
equality-cases (d x y)
(Ξ» (p : x β‘ y) (q : d x y β‘ inl p) β π-elim (n p))
(Ξ» (m : Β¬(x β‘ y)) (q : d x y β‘ inr m) β q β ap inr (nfunext fe (Ξ» (p : x β‘ y) β π-elim (m p))))

isolated-Id-is-prop : {X : π€ Μ } (x : X) β is-isolated' x β (y : X) β is-prop (y β‘ x)
isolated-Id-is-prop x i = local-hedberg' x (Ξ» y β decidable-is-collapsible (i y))

Ξ£-is-discrete : {X : π€ Μ } β {Y : X β π₯ Μ}
β is-discrete X β ((x : X) β is-discrete(Y x)) β is-discrete(Ξ£ Y)
Ξ£-is-discrete {π€} {π₯} {X} {Y} d e (x , y) (x' , y') = g (d x x')
where
g : decidable(x β‘ x') β decidable(x , y β‘ x' , y')
g (inl p) = f (e x' (transport Y p y) y')
where
f : decidable(transport Y p y β‘ y') β decidable((x , y) β‘ (x' , y'))
f (inl q) = inl (to-Ξ£-β‘ (p , q))
f (inr Ο) = inr c
where
c : x , y β‘ x' , y' β π
c r = Ο q
where
p' : x β‘ x'
p' = ap prβ r
q' : transport Y p' y β‘ y'
q' = from-Ξ£-β‘' r
s : p β‘ p'
s = discrete-types-are-sets d p p'
q : transport Y p y β‘ y'
q = ap (Ξ» - β transport Y - y) s β q'
g (inr Ο) = inr (Ξ» q β Ο (ap prβ q))

π-is-set : is-set π
π-is-set = discrete-types-are-sets π-is-discrete

β-is-set : is-set β
β-is-set = discrete-types-are-sets β-is-discrete

nonempty : π€ Μ β π€ Μ
nonempty X = is-empty(is-empty X)

stable : π€ Μ β π€ Μ
stable X = nonempty X β X

decidable-is-stable : {X : π€ Μ } β decidable X β stable X
decidable-is-stable (inl x) Ο = x
decidable-is-stable (inr u) Ο = unique-from-π(Ο u)

stable-is-collapsible : funext π€ π€β β {X : π€ Μ } β stable X β collapsible X
stable-is-collapsible {π€} fe {X} s = (f , g)
where
f : X β X
f x = s(Ξ» u β u x)
claimβ : (x y : X) β (u : is-empty X) β u x β‘ u y
claimβ x y u = unique-from-π(u x)
claimβ : (x y : X) β (Ξ» u β u x) β‘ (Ξ» u β u y)
claimβ x y = dfunext fe (claimβ x y)
g : (x y : X) β f x β‘ f y
g x y = ap s (claimβ x y)

separated-is-Id-collapsible : funext π€ π€β β {X : π€ Μ } β is-separated X β Id-collapsible X
separated-is-Id-collapsible fe s = stable-is-collapsible fe (s _ _)

separated-types-are-sets : funext π€ π€β β {X : π€ Μ } β is-separated X β is-set X
separated-types-are-sets fe s = Id-collapsibles-are-sets (separated-is-Id-collapsible fe s)

is-prop-separated : funext π€ π€ β funext π€ π€β β {X : π€ Μ } β is-prop(is-separated X)
is-prop-separated fe feβ {X} = iprops-are-propositions f
where
f : is-separated X β is-prop(is-separated X)
f s = Ξ -is-prop fe
(Ξ» _ β Ξ -is-prop fe
(Ξ» _ β Ξ -is-prop fe
(Ξ» _ β separated-types-are-sets feβ s)))

\end{code}

Find a better home for this:

\begin{code}

π-β-embedding : π β β
π-β-embedding β = 0
π-β-embedding β = 1

π-β-embedding-lc : left-cancellable π-β-embedding
π-β-embedding-lc {β} {β} refl = refl
π-β-embedding-lc {β} {β} ()
π-β-embedding-lc {β} {β} ()
π-β-embedding-lc {β} {β} refl = refl

C-B-embedding : (β β π) β (β β β)
C-B-embedding Ξ± = π-β-embedding β Ξ±

C-B-embedding-lc : funext π€β π€β β left-cancellable C-B-embedding
C-B-embedding-lc fe {Ξ±} {Ξ²} p = dfunext fe h
where
h : (n : β) β Ξ± n β‘ Ξ² n
h n = π-β-embedding-lc (ap (Ξ» - β - n) p)

\end{code}