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

--------------------------------------------------------------------------------
-- Extension Types in Two-Level Type Theory, auto-formalization root module.
-- See index.agda / index.html for details.
--
-- Typecheck everything with:   make
--
-- Accompanies the paper "Extension Types for Free".  See README.md
-- for the correspondence between modules and the statements of the paper.
--------------------------------------------------------------------------------

module Extension.Everything where

open import Extension.Prelude    -- foundation: Uskuplu's 2LTT library, re-exported
open import Extension.Core       -- Definition 3.1, Lemma 3.2 (RS Fig. 4)
open import Extension.RS         -- Lemma 3.4 (Π), Lemma 3.6 (Σ), Lemma 3.7 (composite)
open import Extension.RSHomotopy -- Lemma 3.11 (strict form) + homotopy ingredient
open import Extension.CofibFibration -- 2LTT §3: is-cofib, Ext-isFibrant, reindex
open import Extension.RS46        -- Lemma 3.11 homotopy form (relative funext), fully proved
open import Extension.RS410       -- Lemma 3.14 homotopy extension property, fully proved
open import Extension.RS48        -- Lemma 3.13 extension extensionality (strict form)
open import Extension.RS412       -- Lemma 3.15 truncation levels: Ext preserves props
open import Extension.FundamentalId -- fundamental theorem of identity types (engine)
open import Extension.PiTruncation -- funext-Id-equiv; cofibrant Πᵉ preserves n-types
open import Extension.SigmaTruncation -- Σ preserves truncation levels (inner HoTT)
open import Extension.RS412Ext    -- Lemma 3.15 for Ext (homotopy, general n-types), full
open import Extension.ExtFamIso   -- Ext-fam-≅: Ext respects a pointwise family iso
open import Extension.RS48Ext     -- Lemma 3.13 for Ext (homotopy): (f=g) ≃ ⟨Extᵢ(λψ.fψ=gψ,refl)⟩
open import Extension.RelFunext   -- Definition 3.9 (= trivial-fibration half), is-cofib-2LTT, Lemma 3.11
open import Extension.WeakStrict  -- total sections as a Σ of extension types
open import Extension.Instances  -- Remark 3.3: proposition-indexed { A ∣ φ ▷ u }
open import Extension.Fibre      -- Lemma 2.2 (strict/homotopy fibre)
open import Extension.CanonicalFibre -- the canonical strict→homotopy fibre map is an equivalence
open import Extension.HomFillers  -- Lemma 2.3: strict fillers ≃ coherent homotopy fillers
open import Extension.Glue        -- pointwise Glue; strict Glue from strict equivalences
open import Extension.GlueStructure -- Definition 4.3 (output triple, strict/homotopy coherence)
open import Extension.GlueRules    -- Remark 4.4, Definition 5.11 (gluing axioms)
open import Extension.UAFromSection -- Lemma 5.10 (univalence engine, via fundamental-id)
open import Extension.Univalence    -- explicit univalence hypothesis and its inverse to idtoeqv
open import Extension.WeakGlueUA   -- Theorem 5.14 (weak glue + coercion laws ⇒ ua)
open import Extension.WeakGlueUAFibrant -- fibrant-interval instance: weak glue ⇒ ua, fully closed
open import Extension.UAStrongGlue -- Theorem 5.4, strong direction (no cofibrancy needed)
open import Extension.GlueStrengthChain3 -- Lemma 5.13(3): htpy-coherent i∂ glue ⇒ weak glue
open import Extension.GlueSandwichFibrant -- glue-sandwich (4)⇒(5)⇒(1) for a fibrant interval
open import Extension.GlueDataFibrant -- Lemma 5.1: GlueData ≅ Extᵢ(W,w₀) (the encoding)
open import Extension.GlueSandwich  -- ua ⇒ GlueData contractible (Theorem 5.4, GlueData form)
open import Extension.CoercionLaws  -- Lemma 5.8 (general path interval) ⇒ weak-glue-implies-ua
open import Extension.GlueSandwichComplete -- Theorem 5.15: (1)⇒(4)⇒(5)⇒(1), fibrant interval
open import Extension.GlueSandwichGeneral -- Theorem 5.15: complete cycle, general path interval
open import Extension.GlueUA      -- a map between contractible types is an equivalence
open import Extension.Conservativity -- Definition 5.6; internal Book/cubical axioms
open import Extension.TheoryComparison -- the implications behind Theorem 6.3: (ua), (int)+(glue)

-- Closure properties, the complete glue packagings, and the conditional pushouts.
open import Extension.CofibClosure  -- composition of 2LTT cofibrations; ∅→B; cofibrant codomains
open import Extension.PropRealign   -- Corollary 3.12: realignment type ≅ Ext, contractible match
open import Extension.RS411         -- RS 4.11: (RS 4.10 + naive RS 4.8) ⇒ RS 4.6
open import Extension.RS410Pack     -- the extension property with both strict boundaries
open import Extension.TriangleStrictification -- Lemma 3.14: strict top, strictly restricting globe
open import Extension.GlueLiteralRules -- Definition 4.1's seven operations on global sections
open import Extension.GlueHomotopySemantic -- Remark 4.4: homotopy rules = strict coherence
open import Extension.GlueSandwichFull -- Theorem 5.15, all five nodes: (1)⇒(2)⇒(3)⇒(4)⇒(5)⇒(1)
open import Extension.CoercionLawsNamed -- Lemma 5.8 named: coe, (c1), (c2), (c3)
open import Extension.ExoPushout    -- exo-pushout interface with strict universal property
open import Extension.RS42          -- Lemma 3.5: pushout-product / currying isos, conditional
open import Extension.RS45          -- Lemma 3.8: union of cofibrations, conditional
open import Extension.CanonicalFillers -- Lemma 2.3: the canonical map is an equivalence
open import Extension.GlueConstructorPackage -- Lemma 4.2: items (4)-(7) ⟺ strict inverse of Θ
open import Extension.Corollary55 -- Corollary 5.5, including constructor package

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

  [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

-}