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

--------------------------------------------------------------------------------
-- Remark 4.4  and  Definition 5.11.
--
-- Two of the gluing-layer definitions, formalized as the type of the
-- data they require (the fibrant universe being the inner universe `UU 𝓤`).
--
--   * `satisfies-homotopy-glue-rules (i,𝓤)`: for every input datum (A,T,f) an
--     output (Glue, p, unglue) with strict boundary and every unglue_ψ an
--     equivalence (Remark 4.4, on items (1)-(3) of Definition 4.1).
--   * `WeakGlue (I,0,1,𝓤)`: the sharply-weakened structure of Definition 5.11:
--     a family, two *paths in the universe*, mere maps, and endpoint homotopies.
--
-- These are definitions, not theorems; they package the axioms the later
-- gluing↔univalence results (Theorem 5.14, Theorem 5.15)
-- range over.
--------------------------------------------------------------------------------

module Extension.GlueRules where

open import Extension.Univalence using (Univalence ; ua-from ; ua-from-β)
open import Extension.Prelude

private
  variable
    ℓφ ℓΨ ℓI : Level

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

module _ {Φ : UUᵉ ℓφ} {Ψ : UUᵉ ℓΨ} (i : Φ → Ψ) (𝓤 : Level) where

  satisfies-homotopy-glue-rules : UUᵉ (ℓφ ⊔ ℓΨ ⊔ lsuc 𝓤)
  satisfies-homotopy-glue-rules =
    (A : Ψ → UU 𝓤) (T : Φ → UU 𝓤) (f : (φ : Φ) → C (T φ ≃ A (i φ)))
    → Σᵉ (Ψ → UU 𝓤) (λ Gl →
      Σᵉ ((λ φ → Gl (i φ)) =ᵉ T) (λ p →
      Σᵉ ((ψ : Ψ) → Gl ψ → A ψ) (λ ung →
      -- boundary (item 3): unglue_{iφ} ≐ f_φ, the map coerced along p.  Maps
      -- between inner types are compared strictly through their conversions `c`.
      Σᵉ ((φ : Φ) → c (ung (i φ))
             =ᵉ exo-tr (λ H → (ξ : Φ) → C (H ξ → A (i ξ))) (exo-inv p)
                       (λ ξ → c (pr1 (ic (f ξ)))) φ)
         (λ _ →
      -- (2) each unglue_ψ is an equivalence
      (ψ : Ψ) → C (isEquiv (ung ψ))))))

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

module _ (I : UUᵉ ℓI) (0I 1I : I) (𝓤 : Level) where

  WeakGlue : UUᵉ (ℓI ⊔ lsuc 𝓤)
  WeakGlue =
    (A B : UU 𝓤) (f : C (A ≃ B))
    → Σᵉ (I → UU 𝓤) (λ G →
      Σᵉ (C (Id (G 0I) A)) (λ b₀ →           -- path in the universe
      Σᵉ (C (Id (G 1I) B)) (λ b₁ →           -- path in the universe
      Σᵉ ((t : I) → C (G t → B)) (λ u →      -- mere maps
      -- (4) endpoint homotopies:  u₀ ∼ f ∘ idtoeqv(b₀),  u₁ ∼ idtoeqv(b₁)
      Σᵉ (C (ic (u 0I) ~ (λ x → pr1 (ic f) (pr1 (idtoeqv (ic b₀)) x)))) (λ _ →
          C (ic (u 1I) ~ pr1 (idtoeqv (ic b₁))))))))

  -- Remark 5.12.  With a univalent universe, the weak structure is
  -- inhabited with no structure on I: take G ≔ λ_.B, b₀ ≔ ua(f)⁻¹, b₁ ≔ refl,
  -- u ≔ λ_.id_B; the endpoint homotopies come from the univalence β-rule.
  private
    -- idtoeqv of a path and of its inverse cancel (path induction).
    idtoeqv-inv-sec : {A B : UU 𝓤} (pth : Id A B) (y : B)
                    → Id (pr1 (idtoeqv pth) (pr1 (idtoeqv (pth ⁻¹)) y)) y
    idtoeqv-inv-sec refl y = refl

  ua-gives-weak-glue : Univalence 𝓤 → WeakGlue
  ua-gives-weak-glue U A B f =
    (λ _ → B)
    ,ᵉ (c ((ua-from U g) ⁻¹)
    ,ᵉ (c refl
    ,ᵉ ((λ _ → c (λ x → x))
    ,ᵉ (c H₀ ,ᵉ c H₁))))
    where
    g : A ≃ B
    g = ic f
    H₀ : (λ (x : B) → x)
       ~ (λ x → pr1 (ic f) (pr1 (idtoeqv (ic (c ((ua-from U g) ⁻¹)))) x))
    H₀ y = (idtoeqv-inv-sec (ua-from U g) y) ⁻¹
           · ap (λ e → pr1 e (pr1 (idtoeqv ((ua-from U g) ⁻¹)) y))
                (ua-from-β U g)
    H₁ : (λ (x : B) → x) ~ pr1 (idtoeqv (ic (c (refl {x = B}))))
    H₁ y = refl