{-

This file contains:

- Eliminator for propositional truncation

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.PropositionalTruncation.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
     : Level
    A B : Type 

recPropTrunc :  {P : Type }  isProp P  (A  P)   A   P
recPropTrunc Pprop f  x           = f x
recPropTrunc Pprop f (squash x y i) =
  Pprop (recPropTrunc Pprop f x) (recPropTrunc Pprop f y) i

propTruncIsProp : isProp  A 
propTruncIsProp x y = squash x y

elimPropTrunc :  {P :  A   Type }  ((a :  A )  isProp (P a)) 
                ((x : A)  P  x )  (a :  A )  P a
elimPropTrunc                 Pprop f  x           = f x
elimPropTrunc {A = A} {P = P} Pprop f (squash x y i) =
  PpropOver (squash x y) (elimPropTrunc Pprop f x) (elimPropTrunc Pprop f y) i
    where
    PpropOver : {a b :  A }  (sq : a  b)   x y  PathP  i  P (sq i)) x y
    PpropOver {a} = J  b (sq : a  b)   x y  PathP  i  P (sq i)) x y) (Pprop a)

-- We could also define the eliminator using the recursor
elimPropTrunc' :  {P :  A   Type }  ((a :  A )  isProp (P a)) 
                 ((x : A)  P  x )  (a :  A )  P a
elimPropTrunc' {P = P} Pprop f a =
  recPropTrunc (Pprop a)  x  transp  i  P (squash  x  a i)) i0 (f x)) a

-- The propositional truncation can be eliminated into non-propositional
-- types as long as the function used in the eliminator is 'coherently
-- constant.' The details of this can be found in the following paper:
--
--   https://arxiv.org/pdf/1411.2682.pdf
module SetElim (Bset : isSet B) where
  Bset' : isSet' B
  Bset' = isSet→isSet' Bset

  recPropTrunc→Set : (f : A  B) (kf : 2-Constant f)   A   B
  helper
    : (f : A  B) (kf : 2-Constant f)  (t u :  A )
     recPropTrunc→Set f kf t  recPropTrunc→Set f kf u

  recPropTrunc→Set f kf  x  = f x
  recPropTrunc→Set f kf (squash t u i) = helper f kf t u i

  helper f kf  x   y  = kf x y
  helper f kf (squash t u i) v
    = Bset' (helper f kf t v) (helper f kf u v) (helper f kf t u) refl i
  helper f kf t (squash u v i)
    = Bset' (helper f kf t u) (helper f kf t v) refl (helper f kf u v) i

  kcomp : ∀(f :  A   B)  2-Constant (f  ∣_∣)
  kcomp f x y = cong f (squash  x   y )

  Fset : isSet (A  B)
  Fset = isSetPi (const Bset)

  Kset : (f : A  B)  isSet (2-Constant f)
  Kset f = isSetPi  _  isSetPi  _  isProp→isSet (Bset _ _)))

  setRecLemma
    : (f :  A   B)
     recPropTrunc→Set (f  ∣_∣) (kcomp f)  f
  setRecLemma f i t
    = elimPropTrunc {P = λ t  recPropTrunc→Set (f  ∣_∣) (kcomp f) t  f t}
         t  Bset _ _)  x  refl) t i

  mkKmap : ( A   B)  Σ (A  B) 2-Constant
  mkKmap f = f  ∣_∣ , kcomp f

  fib : (g : Σ (A  B) 2-Constant)  fiber mkKmap g
  fib (g , kg) = recPropTrunc→Set g kg , refl

  eqv : (g : Σ (A  B) 2-Constant)
        fi  fib g  fi
  eqv g (f , p) =
    ΣProp≡  f  isOfHLevelΣ 2 Fset Kset _ _)
      (cong (uncurry recPropTrunc→Set) (sym p)  setRecLemma f)

  trunc→Set≃ : ( A   B)  (Σ (A  B) 2-Constant)
  trunc→Set≃ .fst = mkKmap
  trunc→Set≃ .snd .equiv-proof g = fib g , eqv g

  -- The strategy of this equivalence proof follows the paper more closely.
  -- It is used further down for the groupoid version, because the above
  -- strategy does not generalize so easily.
  e : B  Σ (A  B) 2-Constant
  e b = const b , λ _ _  refl

  eval : A  (γ : Σ (A  B) 2-Constant)  B
  eval a₀ (g , _) = g a₀

  e-eval :  (a₀ : A) γ  e (eval a₀ γ)  γ
  e-eval a₀ (g , kg) i .fst a₁ = kg a₀ a₁ i
  e-eval a₀ (g , kg) i .snd a₁ a₂ = Bset' refl (kg a₁ a₂) (kg a₀ a₁) (kg a₀ a₂) i

  e-isEquiv : A  isEquiv (e {A = A})
  e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _  refl)

  preEquiv₁ :  A   B  Σ (A  B) 2-Constant
  preEquiv₁ t = e , recPropTrunc (isPropIsEquiv e) e-isEquiv t

  preEquiv₂ : ( A   Σ (A  B) 2-Constant)  Σ (A  B) 2-Constant
  preEquiv₂ = isoToEquiv (iso to const  _  refl) retr)
    where
    to : ( A   Σ (A  B) 2-Constant)  Σ (A  B) 2-Constant
    to f .fst x = f  x  .fst x
    to f .snd x y i = f (squash  x   y  i) .snd x y i

    retr : retract to const
    retr f i t .fst x = f (squash  x  t i) .fst x
    retr f i t .snd x y
      = Bset'
           j  f (squash  x   y  j) .snd x y j)
          (f t .snd x y)
           j  f (squash  x  t j) .fst x)
           j  f (squash  y  t j) .fst y)
          i

  trunc→Set≃₂ : ( A   B)  Σ (A  B) 2-Constant
  trunc→Set≃₂ = compEquiv (equivPi preEquiv₁) preEquiv₂

open SetElim public using (recPropTrunc→Set; trunc→Set≃)

elimPropTrunc→Set
  : {P :  A   Set }
   (∀ t  isSet (P t))
   (f : (x : A)  P  x )
   (kf :  x y  PathP  i  P (squash  x   y  i)) (f x) (f y))
   (t :  A )  P t
elimPropTrunc→Set {A = A} {P = P} Pset f kf t
  = recPropTrunc→Set (Pset t) g gk t
  where
  g : A  P t
  g x = transp  i  P (squash  x  t i)) i0 (f x)

  gk : 2-Constant g
  gk x y i = transp  j  P (squash (squash  x   y  i) t j)) i0 (kf x y i)

RecHProp : (P : A  hProp ) (kP :  x y  P x  P y)   A   hProp 
RecHProp P kP = recPropTrunc→Set isSetHProp P kP

module GpdElim (Bgpd : isGroupoid B) where
  Bgpd' : isGroupoid' B
  Bgpd' = isGroupoid→isGroupoid' Bgpd

  module _ (f : A  B) (3kf : 3-Constant f) where
    open 3-Constant 3kf

    recPropTrunc→Gpd :  A   B
    pathHelper : (t u :  A )  recPropTrunc→Gpd t  recPropTrunc→Gpd u
    triHelper₁
      : (t u v :  A )
       Square refl (pathHelper t u) (pathHelper t v) (pathHelper u v)
    triHelper₂
      : (t u v :  A )
       Square (pathHelper t u) (pathHelper t v) (pathHelper u v) refl

    recPropTrunc→Gpd  x  = f x
    recPropTrunc→Gpd (squash t u i) = pathHelper t u i

    pathHelper  x   y  = link x y
    pathHelper (squash t u j) v = triHelper₂ t u v j
    pathHelper  x  (squash u v j) = triHelper₁  x  u v j

    triHelper₁  x   y   z  = coh₁ x y z
    triHelper₁ (squash s t i) u v
      = Bgpd'
           i  refl)
          (triHelper₂ s t u)
          (triHelper₂ s t v)
           i  pathHelper u v)
          (triHelper₁ s u v)
          (triHelper₁ t u v) i
    triHelper₁  x  (squash t u i) v
      = Bgpd'
           i  refl)
          (triHelper₁  x  t u)
           i  pathHelper  x  v)
          (triHelper₂ t u v)
          (triHelper₁  x  t v)
          (triHelper₁  x  u v)
          i
    triHelper₁  x   y  (squash u v i)
      = Bgpd'
           i  refl)
           i  link x y)
          (triHelper₁  x  u v)
          (triHelper₁  y  u v)
          (triHelper₁  x   y  u)
          (triHelper₁  x   y  v)
          i

    triHelper₂  x   y   z  = coh₂ x y z
    triHelper₂ (squash s t i) u v
      = Bgpd'
          (triHelper₂ s t u)
          (triHelper₂ s t v)
           i  pathHelper u v)
           i  refl)
          (triHelper₂ s u v)
          (triHelper₂ t u v)
          i
    triHelper₂  x  (squash t u i) v
      = Bgpd'
          (triHelper₁  x  t u)
           i  pathHelper  x  v)
          (triHelper₂ t u v)
           i  refl)
          (triHelper₂  x  t v)
          (triHelper₂  x  u v)
          i
    triHelper₂  x   y  (squash u v i)
      = Bgpd'
           i  link x y)
          (triHelper₁  x  u v)
          (triHelper₁  y  u v)
           i  refl)
          (triHelper₂  x   y  u)
          (triHelper₂  x   y  v)
          i

  preEquiv₁ : ( A   Σ (A  B) 3-Constant)  Σ (A  B) 3-Constant
  preEquiv₁ = isoToEquiv (iso fn const  _  refl) retr)
    where
    open 3-Constant

    fn : ( A   Σ (A  B) 3-Constant)  Σ (A  B) 3-Constant
    fn f .fst x = f  x  .fst x
    fn f .snd .link x y i = f (squash  x   y  i) .snd .link x y i
    fn f .snd .coh₁ x y z i j
      = f (squash  x  (squash  y   z  i) j) .snd .coh₁ x y z i j

    retr : retract fn const
    retr f i t .fst x = f (squash  x  t i) .fst x
    retr f i t .snd .link x y j
      = f (squash (squash  x   y  j) t i) .snd .link x y j
    retr f i t .snd .coh₁ x y z
      = Bgpd'
           _  refl)
           k j  f (cb i0 j k) .snd .link x y j)
           k j  f (cb i1 j k) .snd .link x z j)
           k j  f (cb j i1 k) .snd .link y z j)
           k j  f (cb k j i0) .snd .coh₁ x y z k j )
           k j  f (cb k j i1) .snd .coh₁ x y z k j)
          i
      where
      cb : I  I  I   _ 
      cb i j k = squash (squash  x  (squash  y   z  i) j) t k

  e : B  Σ (A  B) 3-Constant
  e b .fst _ = b
  e b .snd = record
           { link = λ _ _ _  b
           ; coh₁ = λ _ _ _ _ _  b
           }

  eval : A  Σ (A  B) 3-Constant  B
  eval a₀ (g , _) = g a₀

  module _ where
    open 3-Constant
    e-eval : ∀(a₀ : A) γ  e (eval a₀ γ)  γ
    e-eval a₀ (g , 3kg) i .fst x = 3kg .link a₀ x i
    e-eval a₀ (g , 3kg) i .snd .link x y = λ j  3kg .coh₁ a₀ x y j i
    e-eval a₀ (g , 3kg) i .snd .coh₁ x y z
      = Bgpd'
           _  refl)
           k j  3kg .coh₁ a₀ x y j k)
           k j  3kg .coh₁ a₀ x z j k)
           k j  3kg .coh₁ a₀ y z j k)
           _ _  g a₀)
          (3kg .coh₁ x y z)
          i

  e-isEquiv : A  isEquiv (e {A = A})
  e-isEquiv a₀ = isoToIsEquiv (iso e (eval a₀) (e-eval a₀) λ _  refl)

  preEquiv₂ :  A   B  Σ (A  B) 3-Constant
  preEquiv₂ t = e , recPropTrunc (isPropIsEquiv e) e-isEquiv t

  trunc→Gpd≃ : ( A   B)  Σ (A  B) 3-Constant
  trunc→Gpd≃ = compEquiv (equivPi preEquiv₂) preEquiv₁

open GpdElim using (recPropTrunc→Gpd; trunc→Gpd≃) public

RecHSet : (P : A  HLevel  2)  3-Constant P   A   HLevel  2
RecHSet P 3kP = recPropTrunc→Gpd (hLevelHLevelSuc 1) P 3kP