{-

The James Construction,
  also known as James Reduced Product

A very fundamental and useful construction in classical homotopy theory.
It can be seen as the free A∞-monoid constructed out of a given type,
namely the "correct higher version" of free monoid that is meaningful for all types,
instead of only h-Sets.

Referrence:
  Guillaume Brunerie,
  "The James construction and Ο€β‚„(π•ŠΒ³) in homotopy type theory"
  (https://arxiv.org/abs/1710.10307)

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

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

private
  variable
    β„“ β„“' : Level

module _
  ((X , xβ‚€) : Pointed β„“) where

  infixr 5 _∷_

  -- The James Construction

  data James : Type β„“ where
    []   : James
    _∷_  : X β†’ James β†’ James
    unit : (xs : James) β†’ xs ≑ xβ‚€ ∷ xs

  Jamesβˆ™ : Pointed β„“
  Jamesβˆ™ = James , []


-- Basic operations on James construction, imitating those in Cubical.Data.List.Base

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

  infixr 5 _++_
  infixl 5 _∷ʳ_

  [_] : X β†’ James Xβˆ™
  [ x ] = x ∷ []

  _++_ : James Xβˆ™ β†’ James Xβˆ™ β†’ James Xβˆ™
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ xs ++ ys
  (unit xs i) ++ ys = unit (xs ++ ys) i

  ++β‚€ : (xs : James Xβˆ™) β†’ xs ≑ xs ++ [ xβ‚€ ]
  ++β‚€ [] = unit []
  ++β‚€ (x ∷ xs) i = x ∷ ++β‚€ xs i
  ++β‚€ (unit xs i) j = unit (++β‚€ xs j) i

  rev : James Xβˆ™ β†’ James Xβˆ™
  rev [] = []
  rev (x ∷ xs) = rev xs ++ [ x ]
  rev (unit xs i) = ++β‚€ (rev xs) i

  _∷ʳ_ : James Xβˆ™ β†’ X β†’ James Xβˆ™
  xs ∷ʳ x = xs ++ x ∷ []

map : {X : Pointed β„“}{Y : Pointed β„“'} β†’ (X β†’βˆ™ Y) β†’ James X β†’ James Y
map f [] = []
map f (x ∷ xs) = f .fst x ∷ map f xs
map f (unit xs i) = (unit (map f xs) βˆ™ (Ξ» i β†’ f .snd (~ i) ∷ map f xs)) i

mapβˆ™ : {X : Pointed β„“}{Y : Pointed β„“'} β†’ (X β†’βˆ™ Y) β†’ Jamesβˆ™ X β†’βˆ™ Jamesβˆ™ Y
mapβˆ™ f .fst = map f
mapβˆ™ f .snd = refl