{-

The Inductive Version of James Construction

This file contains:
  - An inductive family 𝕁, and its direct colimit is equivalence to James;
    (KANG Rongji, Feb. 2022)
  - The family 𝕁 can be iteratively constructed as pushouts;
  - Special cases of 𝕁 n for n = 0, 1 and 2;
  - Connectivity of inclusion maps.

This file is the summary of the main results.
The proof is divided into parts and put inside the fold Cubical.HITs.James.Inductive

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Inductive where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Data.Sequence

open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Pushout.PushoutProduct
open import Cubical.HITs.SequentialColimit

open import Cubical.HITs.James.Base
open import Cubical.HITs.James.Inductive.Base
open import Cubical.HITs.James.Inductive.PushoutFormula
  renaming (isConnectedIncl to connIncl ; isConnectedInl to connInl)
open import Cubical.HITs.James.Inductive.Reduced
open import Cubical.HITs.James.Inductive.ColimitEquivalence

open import Cubical.Homotopy.Connected

private
  variable
    β„“ : Level

module JamesInd
  (Xβˆ™@(X , xβ‚€) : Pointed β„“) where

  -- The family 𝕁 n is equivalence to Brunerie's J n, as will be shown latter.
  -- Instead of his inductive procedure, 𝕁 is defined directly as an indexed HIT.

  𝕁 : β„• β†’ Type β„“
  𝕁 = 𝕁ames (X , xβ‚€)

  -- This family forms a direct system.

  𝕁Seq : Sequence β„“
  𝕁Seq = 𝕁amesSeq (X , xβ‚€)

  -- The inductive construction of James is called π•βˆž.
  -- It is the direct colimit of 𝕁 n.

  π•βˆž : Type β„“
  π•βˆž = SeqColim 𝕁Seq

  -- And of course it is equivalent to James.

  Jβ‰ƒπ•βˆž : James (X , xβ‚€) ≃ π•βˆž
  Jβ‰ƒπ•βˆž = compEquiv (James≃𝕁Red∞ _) (invEquiv (𝕁amesβˆžβ‰ƒπ•Red∞ _))

  -- Special cases of 𝕁 n for n = 0, 1 and 2:

  𝕁₀≃Unit : 𝕁 0 ≃ Unit
  𝕁₀≃Unit = 𝕁ames0≃ _

  𝕁₁≃X : 𝕁 1 ≃ X
  𝕁₁≃X = 𝕁ames1≃ _

  𝕁₂≃P[XΓ—X←X⋁Xβ†’X] : 𝕁 2 ≃ Pushout ⋁β†ͺ fold⋁
  𝕁₂≃P[XΓ—X←X⋁Xβ†’X] = 𝕁ames2≃ _

  -- The following is defined as pushouts of 𝕁 n.

  𝕁Push : β„• β†’ Type β„“
  𝕁Push = 𝕁amesPush (X , xβ‚€)

  -- Brunerie uses f and g to denote the following maps, so do I.

  module _
    {n : β„•} where

    f : 𝕁Push n β†’ X Γ— 𝕁 (1 + n)
    f = leftMap _

    g : 𝕁Push n β†’ 𝕁 (1 + n)
    g = rightMap _

  -- Here we show that 𝕁 (n+2) can be made as double pushouts invoving only X, 𝕁 n and 𝕁 (n+1).
  -- In particular, our 𝕁 is exactly what Brunerie had defined.

  π•β‚™β‚Šβ‚‚β‰ƒPushout : (n : β„•) β†’ 𝕁 (2 + n) ≃ Pushout f g
  π•β‚™β‚Šβ‚‚β‰ƒPushout = 𝕁ames2+n≃ _

  -- Connectivity of inclusion maps:

  module _
    (d : β„•)(conn : isConnected (1 + d) X) where

    -- Warning:
    -- The connectivity is shifted by 2 from the convention of usual homotopy theory.

    -- If X is (d+1)-connected, the transition incl : 𝕁 n β†’ 𝕁 (n+1) will be (n+1)d-connected.

    isConnectedIncl : (n : β„•) β†’ isConnectedFun ((1 + n) Β· d) (incl {n = n})
    isConnectedIncl = connIncl Xβˆ™ d conn

    -- If X is (d+1)-connected, the inclusion inl : 𝕁 n β†’ π•βˆž will be (n+1)d-connected.

    inl∞ : (n : β„•) β†’ 𝕁 n β†’ π•βˆž
    inl∞ _ = incl

    isConnectedInl : (n : β„•) β†’ isConnectedFun ((1 + n) Β· d) (inl∞ n)
    isConnectedInl = connInl Xβˆ™ d conn