{-

This file contains:

- Definition of the Bouquet of circles of a type aka wedge of A circles

-}
module Cubical.HITs.Bouquet.Properties where

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

open import Cubical.Data.Unit

open import Cubical.HITs.Bouquet.Base
open import Cubical.HITs.SphereBouquet
open import Cubical.HITs.Pushout
open import Cubical.HITs.S1

open import Cubical.Homotopy.Loopspace

private
  variable
    ℓ : Level

elimPropBouquet : ∀ {ℓ ℓ'} {A : Type ℓ}
  {B : Bouquet A → Type ℓ'}
  (pr : (x : _) → isProp (B x))
  (b : B base)
  → (x  : Bouquet A) → B x
elimPropBouquet pr b base = b
elimPropBouquet {B = B} pr b (loop x i) =
  isProp→PathP {B = λ i → B (loop x i)} (λ _ → pr _) b b i

module _ {ℓ} {A : Type ℓ} where
  SphereBouquet→Bouquet : SphereBouquet  A → Bouquet A
  SphereBouquet→Bouquet (inl x) = base
  SphereBouquet→Bouquet (inr (s , base)) = base
  SphereBouquet→Bouquet (inr (s , loop i)) = loop s i
  SphereBouquet→Bouquet (push a i) = base

  Bouquet→SphereBouquet : Bouquet A → SphereBouquet  A
  Bouquet→SphereBouquet base = inl tt
  Bouquet→SphereBouquet (loop x i) =
    (push x ∙∙ (λ i → inr (x , loop i)) ∙∙ sym (push x)) i

  Iso-SphereBouquet-Bouquet : Iso (SphereBouquet  A) (Bouquet A)
  Iso.fun Iso-SphereBouquet-Bouquet = SphereBouquet→Bouquet
  Iso.inv Iso-SphereBouquet-Bouquet = Bouquet→SphereBouquet
  Iso.sec Iso-SphereBouquet-Bouquet base = refl
  Iso.sec Iso-SphereBouquet-Bouquet (loop x i) j =
    SphereBouquet→Bouquet
      (doubleCompPath-filler (push x) (λ i → inr (x , loop i)) (sym (push x)) (~ j) i)
  Iso.ret Iso-SphereBouquet-Bouquet (inl x) = refl
  Iso.ret Iso-SphereBouquet-Bouquet (inr (s , base)) = push s
  Iso.ret Iso-SphereBouquet-Bouquet (inr (s , loop i)) j =
    doubleCompPath-filler (push s) (λ i → inr (s , loop i)) (sym (push s)) (~ j) i
  Iso.ret Iso-SphereBouquet-Bouquet (push a i) j = push a (i ∧ j)

  Bouquet≃∙SphereBouquet : SphereBouquet∙  A ≃∙ Bouquet A , base
  fst Bouquet≃∙SphereBouquet = isoToEquiv (Iso-SphereBouquet-Bouquet)
  snd Bouquet≃∙SphereBouquet = refl

module _ {ℓ ℓ'} {A : Type ℓ} (B : Pointed ℓ') where
  BouquetFun∙→Ω : (Bouquet∙ A →∙ B) → (A → Ω B .fst)
  BouquetFun∙→Ω f x = sym (snd f) ∙∙ cong (fst f) (loop x) ∙∙ snd f

  Ω→BouquetFun∙ : (A → Ω B .fst) → (Bouquet∙ A →∙ B)
  fst (Ω→BouquetFun∙ f) base = pt B
  fst (Ω→BouquetFun∙ f) (loop x i) = f x i
  snd (Ω→BouquetFun∙ f) = refl

  CharacBouquet∙Iso : Iso (Bouquet∙ A →∙ B) (A → Ω B .fst)
  Iso.fun CharacBouquet∙Iso = BouquetFun∙→Ω
  Iso.inv CharacBouquet∙Iso = Ω→BouquetFun∙
  Iso.sec CharacBouquet∙Iso h i x j =
    compPath-filler (h x) refl (~ i) j
  fst (Iso.ret CharacBouquet∙Iso h i) base = snd h (~ i)
  fst (Iso.ret CharacBouquet∙Iso h i) (loop x j) =
    doubleCompPath-filler (sym (snd h)) (cong (fst h) (loop x)) (snd h) (~ i) j
  snd (Iso.ret CharacBouquet∙Iso h i) j = snd h (~ i ∨ j)