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

--------------------------------------------------------------------------------
-- Prelude.
--
-- The formalization is built on top of Elif Uskuplu's `2LTT-Agda` library
-- (https://github.com/ElifUskuplu/2LTT-Agda).  We import the non-cumulativity
-- variant `2LTT_C`, which realises the conversion of the paper as an explicit,
-- same-level coercion
--
--     record C {i} (A : UU i) : UUᵉ i   -- constructor  c ,  field  ic : A
--
-- rather than by `--cumulativity` (which makes fibrant→exo coercions spawn
-- underdetermined universe-level metavariables that deadlock inference).
--
-- What the library gives us:
--   * two universes  UU  = Set   (fibrant / inner)   and
--                     UUᵉ = SSet  (exo / strict / outer);
--   * strict (exo) equality  _=ᵉ_  with  reflᵉ,  UIPᵉ,  exo-ap, exo-tr,
--     exo-concat, exo-inv,  happlyᵉ,  and postulated  funextᵉ;
--   * exo Σ / Π  (Σᵉ , _,ᵉ_ , pr1ᵉ , pr2ᵉ , dep-pair-=ᵉ , Πᵉ),  exo isos  _≅_;
--   * the coercion  C / c / ic;  fibrancy  isFibrant  and cofibrancy isCofibrant;
--   * inner HoTT: equivalences  _≃_,  is-contr,  the inner identity type  Id.
--
-- We re-export the whole thing under one name.
--------------------------------------------------------------------------------

module Extension.Prelude where

-- We avoid the top module `2LTT_C.2LTT_C`: it also pulls in the `Types`
-- aggregator and `Diagram_Signatures`, whose transitive contents put Agda
-- 2.8.0's coverage checker into a state where it eagerly (and wrongly) tries to
-- split every explicit argument whose type is a family into a universe,
-- breaking even  f A = A.  The three sub-aggregates below re-export everything
-- we use, including the inner-HoTT layer (Id, is-contr, _≃_, …) via Coercion.

open import 2LTT_C.Exotypes    public  -- Σᵉ, Πᵉ, _=ᵉ_, UIPᵉ, exo-ap, funextᵉ, _≅_, …
open import 2LTT_C.Coercion    public  -- C, c, ic, isFibrant, and inner HoTT
open import 2LTT_C.Cofibration public  -- isCofibrant, isFibration, …

{- References:

  [2LTT-Agda]  Elif Uskuplu.  2LTT-Agda: formalization of 2LTT in Agda.
               https://github.com/ElifUskuplu/2LTT-Agda, commit b064091 (6 August 2025).
               Described in: Elif Uskuplu, Formalizing two-level type theory with
               cofibrant exo-nat, Mathematical Structures in Computer Science 35:e30,
               2025.  doi:10.1017/S0960129525100297

-}