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

--------------------------------------------------------------------------------
-- RS 4.12 for the extension type, homotopy form, general truncation level.
--
--   If every fibre  A ψ  is an n-type, then  Extᵢ(A,a)  is an n-type.
--
-- Same assembly as `Extension.RS46`, with `is-type t` in place of `is-contr`:
-- the total-section space is `is-type t` (`PiTruncation.Πᵉ-preserves-truncation`),
-- the base is `is-type t`, so the fibre, an extension type, is `is-type t`
-- (`SigmaTruncation.Σ-base-fibre-truncation`), via the reindexing.
--------------------------------------------------------------------------------

module Extension.RS412Ext where

open import Extension.Prelude
open import Extension.CofibFibration
open import Extension.PiTruncation using (Πᵉ-preserves-truncation)
open import Extension.SigmaTruncation using (Σ-base-fibre-truncation)
open import Extension.RelFunext using (satisfies-rel-funext)
import Extension.RS48Ext as RS48Ext

private
  variable
    ℓ ℓ' ℓΦ ℓΨ : Level

-- An exo-iso of fibrant types induces an inner equivalence of their matches.
match-equiv : {A : UUᵉ ℓ} {B : UUᵉ ℓ'} (W : isFibrant A) (V : isFibrant B)
            → A ≅ B → fibrant-match W ≃ fibrant-match V
match-equiv W V iso = equiv
  where
  wA = fibrant-witness W
  wB = fibrant-witness V
  j : C (fibrant-match W) ≅ C (fibrant-match V)
  j = ≅-trans (≅-sym wA) (≅-trans iso wB)
  jf  = pr1ᵉ j
  jg  = pr1ᵉ (pr2ᵉ j)
  jgf = pr1ᵉ (pr2ᵉ (pr2ᵉ j))
  jfg = pr2ᵉ (pr2ᵉ (pr2ᵉ j))
  equiv : fibrant-match W ≃ fibrant-match V
  equiv = (λ x → ic (jf (c x)))
        , invertibles-are-equiv _
            ( (λ y → ic (jg (c y)))
            , ( (λ x → =ᵉ-to-Id (jgf (c x)))
              , (λ y → =ᵉ-to-Id (jfg (c y))) ) )

-- Transport a truncation level along such an iso.
Fib-iso-truncation' : (t : 𝕋) {A : UUᵉ ℓ} {B : UUᵉ ℓ'} (W : isFibrant A) (V : isFibrant B)
                    → A ≅ B → is-type t (fibrant-match W) → is-type t (fibrant-match V)
Fib-iso-truncation' t W V iso = is-truncation-cong (≃-sym (match-equiv W V iso)) t

--------------------------------------------------------------------------------
-- RS 4.12 for Ext.
--------------------------------------------------------------------------------

-- The paper quantifies over the external integer n ≥ -2.  An outer index is
-- required here: eliminating the inner type 𝕋 into a motive containing
-- products over arbitrary outer shapes would violate the 2LTT elimination
-- restriction.
data TruncationLevelᵉ : UUᵉ lzero where
  neg-twoᵉ : TruncationLevelᵉ
  succᵉ : TruncationLevelᵉ → TruncationLevelᵉ

decode-level : TruncationLevelᵉ → 𝕋
decode-level neg-twoᵉ = neg-two-𝕋
decode-level (succᵉ t) = succ-𝕋 (decode-level t)

Ext-truncation :
    {Φ : UUᵉ ℓΦ} {Ψ : UUᵉ ℓΨ} {i : Φ → Ψ}
    (cof : is-cofib i ℓ) (triv : satisfies-rel-funext cof)
    (Y : Ψ → UU ℓ) (a : (φ : Φ) → C (Y (i φ))) (t : TruncationLevelᵉ)
  → ((ψ : Ψ) → is-type (decode-level t) (Y ψ))
  → is-type (decode-level t) (fibrant-match (Ext-isFibrant cof Y a))
Ext-truncation cof triv Y a neg-twoᵉ hY = triv Y hY a
Ext-truncation cof triv Y a (succᵉ t) hY f g =
  is-truncation-cong (RS48Ext.RS48Ext cof triv Y a f g) (decode-level t)
    (Ext-truncation cof triv
      (RS48Ext.pointwise-path cof triv Y a f g)
      (RS48Ext.pointwise-boundary cof triv Y a f g) t
      (λ ψ → hY ψ (RS48Ext.value cof triv Y a f ψ)
                       (RS48Ext.value cof triv Y a g ψ)))

{- 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

-}