open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Foundations.Path

open import Cubical.Data.Equality using (id)
open import Cubical.Data.Sigma


module Modality.Glue (ABS : Type) (ABS-isProp : isProp ABS) where

open import Modality.Abstract ABS ABS-isProp
open import Modality.Concrete ABS ABS-isProp

-- Note: `Glue' {X-⊤} {X-abs} α` is what is written in the paper as `Glue(● X-⊤, ◯ X-abs, ● (η∘ ∘ α))`.
-- In this work, we only use this special case, not the more general `Glue`.
Glue' : {X-⊤ X-abs : Type} → (X-⊤ → X-abs) → Type
Glue' {X-⊤} {X-abs} α = Σ[ x• ∈ ● X-⊤ ] Σ[ x∘ ∈ ◯ X-abs ] ●-map (η∘ ∘ α) x• ≡ η• x∘

square : ∀ {X-⊤ X-abs α Y-⊤ Y-abs β} (f-⊤ : X-⊤ → Y-⊤) (f-abs : X-abs → Y-abs)
  → β ∘ f-⊤ ≡ f-abs ∘ α
  → Glue' α
  → Glue' β
square {X-⊤} {X-abs} {α} {Y-⊤} {Y-abs} {β} f-⊤ f-abs f-correct (x• , x∘ , h) =
  ●-map f-⊤ x• ,
  ◯-map f-abs x∘ ,
  ( ●-map (η∘ ∘ β) (●-map f-⊤ x•)
  ≡⟨ congS (_$ x•) ●-map-∘ ⟩
    ●-map (η∘ ∘ β ∘ f-⊤) x•
  ≡⟨ congS (λ f → ●-map (η∘ ∘ f) x•) f-correct ⟩
    ●-map (η∘ ∘ f-abs ∘ α) x•
  ≡⟨ congS (λ f → ●-map (f ∘ α) x•) (η∘-isNatural f-abs) ⟩
    ●-map (◯-map f-abs ∘ η∘ ∘ α) x•
  ≡⟨ sym (congS (_$ x•) ●-map-∘) ⟩
    ●-map (◯-map f-abs) (●-map (η∘ ∘ α) x•)
  ≡⟨ congS (●-map (◯-map f-abs)) h ⟩
    ●-map (◯-map f-abs) (η• x∘)
  ≡⟨ refl ⟩
    η• (◯-map f-abs x∘)
  ∎)

triangle : ∀ {Y-⊤ Y-abs β} (e-⊤ : Y-⊤) (e-abs : Y-abs)
  → β e-⊤ ≡ e-abs
  → Glue' β
triangle e-⊤ e-abs e-correct =
  η• e-⊤ ,
  η∘ e-abs ,
  congS (η• ∘ η∘) e-correct

◯Glue' : ∀ {X-⊤} {X-abs} (α : X-⊤ → X-abs) → ABS → Glue' α ≃ X-abs
◯Glue' {X-⊤} {X-abs} α abs =
    (Σ[ x• ∈ ● X-⊤ ] Σ[ x∘ ∈ ◯ X-abs ] ●-map (η∘ ∘ α) x• ≡ η• x∘)
  ≃⟨ Σ-contractFst (◯●-isContr abs) ⟩
    (Σ[ x∘ ∈ ◯ X-abs ] ●-map (η∘ ∘ α) (◯●-isContr abs .fst) ≡ η• x∘)
  ≃⟨ Σ-contractSnd (λ x∘ → isProp→isContrPath (isContr→isProp (◯●-isContr abs)) _ _) ⟩
    ◯ X-abs
  ≃⟨ ◯-X≃◯X abs ⟩
    X-abs
  ■

glue : ∀ {X} → Glue' {X} id → X
glue = uncurry (●-ind _ η•-case ∗-case law-case)
  module glue where
    η•-case = λ x (x∘ , h) → ●-ind (const _) (const x) x∘ (λ h' abs → cong (_$ abs) h') (●-lex h)
    ∗-case = λ abs (x∘ , h) → x∘ abs
    law-case = λ x abs → funext-dep-i0 λ (x∘ , h) →
        ◯●-indP (const _) _ _ (●-lex h) abs
      ∙ sym (cong (_$ abs) (transportRefl x∘))
      where
        -- The following two proofs are imported from the 1Lab: https://1lab.dev/1Lab.Type.Pi.html
        funext-dep
          : ∀ {A : I → Type} {B : (i : I) → A i → Type} {f g}
          → ( ∀ {x₀ x₁} (p : PathP A x₀ x₁)
            → PathP (λ i → B i (p i)) (f x₀) (g x₁) )
          → PathP (λ i → (x : A i) → B i x) f g
        funext-dep {A = A} {B} h i x =
          transp (λ k → B i (coei→i A i x k)) (i ∨ ~ i)
            (h (λ j → coei→j A i j x) i)

        funext-dep-i0
          : ∀ {A : I → Type} {B : (i : I) → A i → Type} {f g}
          → ( ∀ (x : A i0)
            → PathP (λ i → B i (coe0→i A i x)) (f x) (g (coe0→1 A x)))
          → PathP (λ i → (x : A i) → B i x) f g
        funext-dep-i0 {A = A} {B} {f} {g} h =
          funext-dep λ {x₀} {x₁} p →
          subst (λ (p : (i : I) → A i) → PathP (λ i → B i (p i)) (f (p i0)) (g (p i1)))
            (λ j i → coePath A (λ i → p i) i0 i j)
            (h x₀)

◯glue : ∀ {X} → (g : Glue' {X} id) (abs : ABS) → glue g ≡ fst (snd g) abs
◯glue (x• , x') abs = cong (_$ x') $
    fromPathP⁻ (◯●-indP η•-case ∗-case law-case x• abs)
  ∙ transportRefl λ (x∘ , _) → x∘ abs
  where open glue