Martin Escardo and Tom de Jong, October 2021

Modified from UF.PropTrunc.lagda to add the parameter F.

We use F to control the universe where propositional truncations live.
For more comments and explanations, see the original files.

\begin{code}

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

open import MLTT.Spartan

module UF.PropTrunc-Variation (F : Universe β†’ Universe) where

open import MLTT.Plus-Properties
open import UF.Subsingletons
open import UF.FunExt
open import UF.Subsingletons-FunExt
open import UF.Equiv

record propositional-truncations-exist : 𝓀ω where
 field
  βˆ₯_βˆ₯ : {𝓀 : Universe} β†’ 𝓀 Μ‡ β†’ F 𝓀 Μ‡
  βˆ₯βˆ₯-is-prop : {𝓀 : Universe} {X : 𝓀 Μ‡ } β†’ is-prop βˆ₯ X βˆ₯
  ∣_∣ : {𝓀 : Universe} {X : 𝓀 Μ‡ } β†’ X β†’ βˆ₯ X βˆ₯
  βˆ₯βˆ₯-rec : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡ } {P : π“₯ Μ‡ } β†’ is-prop P β†’ (X β†’ P) β†’ βˆ₯ X βˆ₯ β†’ P
 infix 0 βˆ₯_βˆ₯
 infix 0 ∣_∣

module PropositionalTruncation (pt : propositional-truncations-exist) where

 open propositional-truncations-exist pt public

 βˆ₯βˆ₯-induction : {X : 𝓀 Μ‡ } {P : βˆ₯ X βˆ₯ β†’ π“₯ Μ‡ }
             β†’ ((s : βˆ₯ X βˆ₯) β†’ is-prop (P s))
             β†’ ((x : X) β†’ P ∣ x ∣)
             β†’ (s : βˆ₯ X βˆ₯) β†’ P s

 βˆ₯βˆ₯-induction {𝓀} {π“₯} {X} {P} i f s = Ο†' s
  where
   Ο† : X β†’ P s
   Ο† x = transport P (βˆ₯βˆ₯-is-prop ∣ x ∣ s) (f x)
   Ο†' : βˆ₯ X βˆ₯ β†’ P s
   Ο†' = βˆ₯βˆ₯-rec (i s) Ο†


 is-singleton'-is-prop : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀 β†’ is-prop (is-prop X Γ— βˆ₯ X βˆ₯)
 is-singleton'-is-prop fe = Ξ£-is-prop (being-prop-is-prop fe) (Ξ» _ β†’ βˆ₯βˆ₯-is-prop)

 the-singletons-are-the-inhabited-propositions : {X : 𝓀 Μ‡ } β†’ is-singleton X ↔ is-prop X Γ— βˆ₯ X βˆ₯
 the-singletons-are-the-inhabited-propositions {𝓀} {X} = f , g
  where
   f : is-singleton X β†’ is-prop X Γ— βˆ₯ X βˆ₯
   f (x , Ο†) = singletons-are-props (x , Ο†) , ∣ x ∣

   g : is-prop X Γ— βˆ₯ X βˆ₯ β†’ is-singleton X
   g (i , s) = βˆ₯βˆ₯-rec i id s , i (βˆ₯βˆ₯-rec i id s)

 βˆ₯βˆ₯-functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ Y βˆ₯
 βˆ₯βˆ₯-functor f = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» x β†’ ∣ f x ∣)

 βˆ₯βˆ₯-recβ‚‚ : {𝓀 π“₯ : Universe} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {P : 𝓦 Μ‡ }
         β†’ is-prop P β†’ (X β†’ Y β†’ P) β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ Y βˆ₯ β†’ P
 βˆ₯βˆ₯-recβ‚‚ i f s t = βˆ₯βˆ₯-rec i (Ξ» x β†’ βˆ₯βˆ₯-rec i (f x) t) s

 βˆ₯βˆ₯-functorβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
             β†’ (X β†’ Y β†’ Z) β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ Y βˆ₯ β†’ βˆ₯ Z βˆ₯
 βˆ₯βˆ₯-functorβ‚‚ f s t = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» x β†’ βˆ₯βˆ₯-functor (f x) t) s

 βˆƒ : {X : 𝓀 Μ‡ } (Y : X β†’ π“₯ Μ‡ ) β†’ F (𝓀 βŠ” π“₯) Μ‡
 βˆƒ Y = βˆ₯ Ξ£ Y βˆ₯

 βˆƒ-is-prop : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } β†’ is-prop (βˆƒ Y)
 βˆƒ-is-prop = βˆ₯βˆ₯-is-prop

 Exists : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ F (𝓀 βŠ” π“₯) Μ‡
 Exists X Y = βˆƒ Y

 syntax Exists A (Ξ» x β†’ b) = βˆƒ x κž‰ A , b

 infixr -1 Exists

 _∨_  : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ F (𝓀 βŠ” π“₯) Μ‡
 P ∨ Q = βˆ₯ P + Q βˆ₯

 ∨-is-prop  : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } β†’ is-prop (P ∨ Q)
 ∨-is-prop = βˆ₯βˆ₯-is-prop


 left-fails-gives-right-holds : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } β†’ is-prop Q β†’ P ∨ Q β†’ Β¬ P β†’ Q
 left-fails-gives-right-holds i d u = βˆ₯βˆ₯-rec i (Ξ» d β†’ Left-fails-gives-right-holds d u) d

 right-fails-gives-left-holds : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } β†’ is-prop P β†’ P ∨ Q β†’ Β¬ Q β†’ P
 right-fails-gives-left-holds i d u = βˆ₯βˆ₯-rec i (Ξ» d β†’ Right-fails-gives-left-holds d u) d

 pt-gdn : {X : 𝓀 Μ‡ } β†’ βˆ₯ X βˆ₯ β†’ βˆ€ {π“₯} (P : π“₯ Μ‡ ) β†’ is-prop P β†’ (X β†’ P) β†’ P
 pt-gdn {𝓀} {X} s {π“₯} P isp u = βˆ₯βˆ₯-rec isp u s

 gdn-pt : {X : 𝓀 Μ‡ } β†’ (βˆ€ {π“₯} (P : π“₯ Μ‡ ) β†’ is-prop P β†’ (X β†’ P) β†’ P) β†’ βˆ₯ X βˆ₯
 gdn-pt {𝓀} {X} Ο† = Ο† βˆ₯ X βˆ₯ βˆ₯βˆ₯-is-prop ∣_∣

 inhabited-is-nonempty : {X : 𝓀 Μ‡ } β†’ βˆ₯ X βˆ₯ β†’ ¬¬ X
 inhabited-is-nonempty s = pt-gdn s 𝟘 𝟘-is-prop

 uninhabited-is-empty : {X : 𝓀 Μ‡ } β†’ Β¬ βˆ₯ X βˆ₯ β†’ Β¬ X
 uninhabited-is-empty u x = u ∣ x ∣

 empty-is-uninhabited : {X : 𝓀 Μ‡ } β†’ Β¬ X β†’ Β¬ βˆ₯ X βˆ₯
 empty-is-uninhabited v = βˆ₯βˆ₯-rec 𝟘-is-prop v

 binary-choice : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ βˆ₯ X βˆ₯ β†’ βˆ₯ Y βˆ₯ β†’ βˆ₯ X Γ— Y βˆ₯
 binary-choice s t = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» x β†’ βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop (Ξ» y β†’ ∣ x , y ∣) t) s

 prop-is-equivalent-to-its-truncation : {X : 𝓀 Μ‡ } β†’ is-prop X β†’ βˆ₯ X βˆ₯ ≃ X
 prop-is-equivalent-to-its-truncation i =
  logically-equivalent-props-are-equivalent βˆ₯βˆ₯-is-prop i (βˆ₯βˆ₯-rec i id) ∣_∣

 _>>=_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ βˆ₯ X βˆ₯ β†’ (X β†’ βˆ₯ Y βˆ₯) β†’ βˆ₯ Y βˆ₯
 s >>= f = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop f s

 infixr 0 _∨_

\end{code}