{-# OPTIONS --without-K --exact-split --two-level #-}

--------------------------------------------------------------------------------
-- RS 4.12 (truncation levels), the propositional case.
--
--   If every fibre  A ψ  is a proposition, then  Extᵢ(A,a)  is a proposition.
--
-- This case does not need the identity-type characterization (RS 4.8 homotopy):
-- an *inhabited* proposition is contractible, so it follows directly from RS 4.6
-- (`Extension.RS46`).  The higher truncation levels (`is-set`, …) genuinely need
-- the identity type of the fibrant match of Ext as an extension type, see README.
--------------------------------------------------------------------------------

module Extension.RS412 where

open import Extension.Prelude
open import Extension.Core
open import Extension.CofibFibration
open import Extension.RS46

private
  variable
    ℓ ℓΦ ℓΨ : Level

-- An inhabited proposition is contractible.
inhabited-prop-contr : {A : UU ℓ} → is-prop A → A → is-contr A
inhabited-prop-contr p a = a , (λ x → center _ (p x a))

-- To be a proposition it suffices to be contractible whenever inhabited.
prop-if-inhabited-contr : {A : UU ℓ} → (A → is-contr A) → is-prop A
prop-if-inhabited-contr f a' a = is-prop-is-contr _ (f a') a' a

--------------------------------------------------------------------------------
-- RS 4.12, propositional case.
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
         (cof : is-cofib i ℓ) (cofΨ : isCofibrant Ψ ℓ) (cofΦ : isCofibrant Φ ℓ)
         (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ)))
       where

  private
    -- an element of the match yields an inhabitant of the extension type
    inhab : fibrant-match (Ext-isFibrant cof Y a) → Ext i (λ ψ → C (Y ψ)) a
    inhab w = pr1ᵉ (pr2ᵉ (fibrant-witness (Ext-isFibrant cof Y a))) (c w)

  Ext-is-prop : ((ψ : Ψ) → is-prop (Y ψ))
              → Fib-is-prop (Ext i (λ ψ → C (Y ψ)) a) {Ext-isFibrant cof Y a}
  Ext-is-prop pY =
    prop-if-inhabited-contr
      (λ w → RS46 cof cofΨ cofΦ Y
               (λ ψ → inhabited-prop-contr (pY ψ) (ic (ext-app (inhab w) ψ))) a)

{- References:

  [RS]         Emily Riehl and Michael Shulman.  A type theory for synthetic
               ∞-categories.  Higher Structures 1(1):147-224, 2017.
               doi:10.21136/hs.2017.06

-}