Ian Ray, 2 June 2024

Modification by Martin Escardo and Tom de Jong 12th September 2024.

Minor modifications by Tom de Jong on 4 September 2024

Modifications by Ian Ray on 17th December 2024.

We develop n-types, or n-truncated types, as defined in the HoTT book.

In this file we will assume function extensionality globally but not
univalence.  The final result of the file will be proved in the local
presence of univalence.

\begin{code}

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

open import UF.FunExt

module UF.TruncatedTypes
        (fe : Fun-Ext)
       where

open import MLTT.Spartan hiding (_+_)

open import Notation.Order
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Retracts
open import UF.Singleton-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.TruncationLevels
open import UF.Univalence

private
 fe' : FunExt
 fe' 𝓀 π“₯ = fe {𝓀} {π“₯}

_is_truncated : 𝓀 Μ‡ β†’ β„•β‚‹β‚‚ β†’ 𝓀 Μ‡
X is βˆ’2 truncated       = is-contr X
X is (succ n) truncated = (x x' : X) β†’ (x ＝ x') is n truncated

_is_truncated-map : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (f : X β†’ Y) β†’ β„•β‚‹β‚‚ β†’ 𝓀 βŠ” π“₯ Μ‡
f is n truncated-map = each-fiber-of f (Ξ» - β†’ - is n truncated)

being-truncated-is-prop : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ }
                        β†’ is-prop (X is n truncated)
being-truncated-is-prop {_} {βˆ’2} = being-singleton-is-prop fe
being-truncated-is-prop {_} {succ n} =
 Ξ β‚‚-is-prop fe (Ξ» x x' β†’ being-truncated-is-prop)

being-truncated-map-is-prop : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {f : X β†’ Y}
                            β†’ is-prop (f is n truncated-map)
being-truncated-map-is-prop = Ξ -is-prop fe (Ξ» y β†’ being-truncated-is-prop)

\end{code}

Being -1-truncated is equivalent to being a proposition.

\begin{code}

is-prop' : (X : 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
is-prop' X = X is βˆ’1 truncated

being-prop'-is-prop : (X : 𝓀 Μ‡ ) β†’ is-prop (is-prop' X)
being-prop'-is-prop X = being-truncated-is-prop

is-prop-implies-is-prop' : {X : 𝓀 Μ‡ } β†’ is-prop X β†’ is-prop' X
is-prop-implies-is-prop' X-is-prop x x' =
 pointed-props-are-singletons (X-is-prop x x') (props-are-sets X-is-prop)

is-prop'-implies-is-prop : {X : 𝓀 Μ‡ } β†’ is-prop' X β†’ is-prop X
is-prop'-implies-is-prop X-is-prop' x x' = center (X-is-prop' x x')

is-prop-equiv-is-prop' : {X : 𝓀 Μ‡ } β†’ is-prop X ≃ is-prop' X
is-prop-equiv-is-prop' {𝓀} {X} =
 logically-equivalent-props-are-equivalent (being-prop-is-prop fe)
                                           (being-prop'-is-prop X)
                                           is-prop-implies-is-prop'
                                           is-prop'-implies-is-prop

\end{code}

Truncation levels are upper closed.

\begin{code}

contractible-types-are-props' : {X : 𝓀 Μ‡ } β†’ is-contr X β†’ is-prop' X
contractible-types-are-props' = is-prop-implies-is-prop' ∘ singletons-are-props

truncation-levels-are-upper-closed : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ }
                                   β†’ X is n truncated
                                   β†’ X is (n + 1) truncated
truncation-levels-are-upper-closed {𝓀} {βˆ’2} = contractible-types-are-props'
truncation-levels-are-upper-closed {𝓀} {succ n} t x x' =
 truncation-levels-are-upper-closed (t x x')

truncation-levels-are-upper-closed-+ : {n : β„•β‚‹β‚‚} {l : β„•} {X : 𝓀 Μ‡ }
                                    β†’ X is n truncated
                                    β†’ X is n + l truncated
truncation-levels-are-upper-closed-+ {_} {n} {zero} {X} X-n-trunc = X-n-trunc
truncation-levels-are-upper-closed-+ {_} {n} {succ l} {X} X-n-trunc =
 truncation-levels-are-upper-closed
  (truncation-levels-are-upper-closed-+ X-n-trunc)

truncation-levels-are-upper-closed' : {n n' : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ }
                                    β†’ n ≀ n'
                                    β†’ X is n truncated
                                    β†’ X is n' truncated
truncation-levels-are-upper-closed' {_} {n} {n'} {X} o X-n-trunc =
 transport (Ξ» - β†’ X is - truncated) p
           (truncation-levels-are-upper-closed-+ X-n-trunc)
 where
  m : β„•
  m = subtraction-β„•β‚‹β‚‚-term n n' o
  p = n + m   ＝⟨ subtraction-β„•β‚‹β‚‚-identification n n' o ⟩
      n'      ∎

truncation-levels-closed-under-Id : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ }
                                  β†’ X is n truncated
                                  β†’ (x x' : X) β†’ (x ＝ x') is n truncated
truncation-levels-closed-under-Id {𝓀} {βˆ’2} = contractible-types-are-props'
truncation-levels-closed-under-Id {𝓀} {succ n} t x x' =
 truncation-levels-are-upper-closed (t x x')

\end{code}

We will now give some closure results about truncation levels.

\begin{code}

truncated-types-are-closed-under-retracts : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                          β†’ retract X of Y
                                          β†’ Y is n truncated
                                          β†’ X is n truncated
truncated-types-are-closed-under-retracts {𝓀} {π“₯} {βˆ’2} {X} {Y} =
 retract-of-singleton
truncated-types-are-closed-under-retracts {𝓀} {π“₯} {succ n} (r , s , H) t x x' =
 truncated-types-are-closed-under-retracts
  (＝-retract s (r , H) x x')
  (t (s x) (s x'))

truncated-types-closed-under-equiv : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                   β†’ X ≃ Y
                                   β†’ Y is n truncated
                                   β†’ X is n truncated
truncated-types-closed-under-equiv e =
 truncated-types-are-closed-under-retracts (≃-gives-◁ e)

\end{code}

We can prove closure under embeddings as a consequence of the previous
result.

\begin{code}

truncated-types-closed-under-embedding⁺ : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                        β†’ X β†ͺ Y
                                        β†’ Y is (n + 1) truncated
                                        β†’ X is (n + 1) truncated
truncated-types-closed-under-embedding⁺ {𝓀} {π“₯} (e , is-emb) t x x' =
 truncated-types-closed-under-equiv
  (ap e , embedding-gives-embedding' e is-emb x x')
  (t (e x) (e x'))

truncated-types-closed-under-embedding : {n : β„•β‚‹β‚‚}
                                       β†’ n β‰₯ βˆ’1
                                       β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                       β†’ X β†ͺ Y
                                       β†’ Y is n truncated
                                       β†’ X is n truncated
truncated-types-closed-under-embedding {𝓀} {π“₯} {succ n} _ =
 truncated-types-closed-under-embedding⁺

\end{code}

Using closure under equivalence we can show closure under Ξ£ and Ξ .

\begin{code}

truncated-types-closed-under-Ξ£ : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } (Y : X β†’ π“₯ Μ‡ )
                               β†’ X is n truncated
                               β†’ ((x : X) β†’ (Y x) is n truncated)
                               β†’ (Ξ£ Y) is n truncated
truncated-types-closed-under-Ξ£ {𝓀} {π“₯} {βˆ’2} Y = Ξ£-is-singleton
truncated-types-closed-under-Ξ£ {𝓀} {π“₯} {succ n} Y l m (x , y) (x' , y') =
 truncated-types-closed-under-equiv Ξ£-＝-≃
  (truncated-types-closed-under-Ξ£
   (Ξ» p β†’ transport Y p y ＝ y')
   (l x x')
   (Ξ» p β†’ m x' (transport Y p y) y'))

truncated-types-closed-under-Ξ  : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } (Y : X β†’ π“₯ Μ‡ )
                               β†’ ((x : X) β†’ (Y x) is n truncated)
                               β†’ (Ξ  Y) is n truncated
truncated-types-closed-under-Ξ  {𝓀} {π“₯} {βˆ’2} Y = Ξ -is-singleton fe
truncated-types-closed-under-Ξ  {𝓀} {π“₯} {succ n} Y m f g =
 truncated-types-closed-under-equiv (happly-≃ fe)
  (truncated-types-closed-under-Ξ  (Ξ» x β†’ f x ＝ g x)
  (Ξ» x β†’ m x (f x) (g x)))

truncated-types-closed-under-β†’ : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                               β†’ Y is n truncated
                               β†’ (X β†’ Y) is n truncated
truncated-types-closed-under-β†’ {𝓀} {π“₯} {n} {X} {Y} m =
 truncated-types-closed-under-Ξ  (Ξ» - β†’ Y) (Ξ» - β†’ m)

\end{code}

The subuniverse of types of n truncated types is defined as follows.

\begin{code}

𝕋 : β„•β‚‹β‚‚ β†’ (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
𝕋 n 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , X is n truncated

\end{code}

From univalence we can show that 𝕋 n is n + 1 truncated,
for all n : β„•β‚‹β‚‚.

\begin{code}

truncation-levels-closed-under-≃⁺ : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                  β†’ Y is (n + 1) truncated
                                  β†’ (X ≃ Y) is (n + 1) truncated
truncation-levels-closed-under-≃⁺ {𝓀} {π“₯} {n} {X} {Y} tY =
 truncated-types-closed-under-embedding ⋆ (equiv-embeds-into-function fe')
  (truncated-types-closed-under-Ξ  (Ξ» _ β†’ Y) (Ξ» _ β†’ tY))

truncation-levels-closed-under-≃ : {n : β„•β‚‹β‚‚} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                                 β†’ X is n truncated
                                 β†’ Y is n truncated
                                 β†’ (X ≃ Y) is n truncated
truncation-levels-closed-under-≃ {𝓀} {π“₯} {βˆ’2} = ≃-is-singleton fe'
truncation-levels-closed-under-≃ {𝓀} {π“₯} {succ n} tX =
 truncation-levels-closed-under-≃⁺

𝕋-is-of-next-truncation-level : {n : β„•β‚‹β‚‚} {𝓀 : Universe}
                              β†’ is-univalent 𝓀
                              β†’ (𝕋 n 𝓀) is (n + 1) truncated
𝕋-is-of-next-truncation-level ua (X , l) (Y , l') =
 truncated-types-closed-under-equiv I (truncation-levels-closed-under-≃ l l')
 where
  I = ((X , l) ＝ (Y , l')) β‰ƒβŸ¨ II ⟩
       (X ＝ Y)             β‰ƒβŸ¨ univalence-≃ ua X Y ⟩
       (X ≃ Y)              β– 
   where
    II = ≃-sym (to-subtype-＝-≃ (Ξ» _ β†’ being-truncated-is-prop))

\end{code}