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}