open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base renaming (Bool to Bool₂ ; true to true₂ ; false to false₂)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool.Properties using (isSetBool)
open import Cubical.Foundations.HLevels using (isSetΣ)

open import DPRLR.Cubical.Path using (ΣPathP-subst)
open import DPRLR.Simplicial.Product using (Σ≤)
open import DPRLR.Simplicial.Hom
open import DPRLR.Simplicial.Contravariant
open import DPRLR.Simplicial.Discrete
open import DPRLR.Simplicial.PreorderLocalization using (⌞_⌟)
open import DPRLR.Object.Model.Model

module DPRLR.Gluing.LogicalRelations.Bool
  {ℓS ℓM : Level} (𝓜 : SimpleCwF ℓS ℓM) where
  open import DPRLR.Gluing.LogicalRelations.Judgment 𝓜
  open import DPRLR.Gluing.LogicalRelations.Substitution 𝓜
  open import DPRLR.Gluing.Base 𝓜

  ⌜_⌝ : Bool₂ → ⌞ Tmₘ εₘ Boolₘ ⌟
  ⌜ true₂ ⌝ = trueₘ
  ⌜ false₂ ⌝ = falseₘ

  BOOL∙ : ⌞ Tmₘ εₘ Boolₘ ⌟ → Type ℓM
  BOOL∙ M =
    Σ Bool₂ (λ b → M ≤ ⌜ b ⌝)

  BOOL-contravariant :
    isContravariant BOOL∙
  BOOL-contravariant =
    contravariant-Σ-discrete Bool₂-isDiscrete λ b →
      representable-isContravariant (tm-segalₘ εₘ Boolₘ) ⌜ b ⌝

  BOOL : GluTy
  GluTy.A° BOOL = Boolₘ
  GluTy.A∙ BOOL M = BOOL∙ M ,
    isSetΣ isSetBool λ b → isProp→isSet (tm-thinₘ εₘ Boolₘ M ⌜ b ⌝)
  GluTy.cA BOOL = BOOL-contravariant

  TRUE∙ :
    {Γ : GluCtx}
    (γ° : ⌞ Subₘ εₘ (GluCtx.Γ° Γ) ⌟)
    (γ∙ : ⌞ GluCtx.Γ∙ Γ γ° ⌟)
    → BOOL∙ (trueₘ [ γ° ]Tmₘ)
  TRUE∙ γ° _ =
    true₂ , path→hom (true[]ₘ γ°)

  FALSE∙ :
    {Γ : GluCtx}
    (γ° : ⌞ Subₘ εₘ (GluCtx.Γ° Γ) ⌟)
    (γ∙ : ⌞ GluCtx.Γ∙ Γ γ° ⌟)
    → BOOL∙ (falseₘ [ γ° ]Tmₘ)
  FALSE∙ γ° _ =
    false₂ , path→hom (false[]ₘ γ°)

  TRUE :
    {Γ : GluCtx}
    → GluTm Γ BOOL
  GluTm.M° TRUE = trueₘ
  GluTm.M∙ (TRUE {Γ = Γ}) = TRUE∙ {Γ = Γ}

  FALSE :
    {Γ : GluCtx}
    → GluTm Γ BOOL
  GluTm.M° FALSE = falseₘ
  GluTm.M∙ (FALSE {Γ = Γ}) = FALSE∙ {Γ = Γ}

  TRUE₀ FALSE₀ : GluTm₀ BOOL
  TRUE₀ = trueₘ , true₂ , hom-refl trueₘ
  FALSE₀ = falseₘ , false₂ , hom-refl falseₘ

  TRUE[]₀ : {Γ : GluCtx} (γ : GluSub₀ Γ) → TRUE {Γ = Γ} [ γ ]Tm₀ ≡ TRUE₀
  TRUE[]₀ (γ , γ∙) = ΣPathP (true[]ₘ γ , λ i → true₂ , arrow i)
    where
    arrow : PathP (λ i → true[]ₘ γ i ≤ trueₘ)
      (path→hom (true[]ₘ γ)) (hom-refl trueₘ)
    arrow = isProp→PathP (λ i → tm-thinₘ εₘ Boolₘ (true[]ₘ γ i) trueₘ)
      (path→hom (true[]ₘ γ)) (hom-refl trueₘ)

  FALSE[]₀ : {Γ : GluCtx} (γ : GluSub₀ Γ) → FALSE {Γ = Γ} [ γ ]Tm₀ ≡ FALSE₀
  FALSE[]₀ (γ , γ∙) = ΣPathP (false[]ₘ γ , λ i → false₂ , arrow i)
    where
    arrow : PathP (λ i → false[]ₘ γ i ≤ falseₘ)
      (path→hom (false[]ₘ γ)) (hom-refl falseₘ)
    arrow = isProp→PathP (λ i → tm-thinₘ εₘ Boolₘ (false[]ₘ γ i) falseₘ)
      (path→hom (false[]ₘ γ)) (hom-refl falseₘ)

  TRUE[] : {Γ Δ : GluCtx} (σ : GluSub Γ Δ)
    → (TRUE {Γ = Δ}) [ σ ]Tmᵍ ≡ TRUE {Γ = Γ}
  TRUE[] {Γ} {Δ} σ = GluTm-ext (true[]ₘ (GluSub.σ° σ)) λ γ →
      (TRUE [ σ ]Tmᵍ) [ γ ]Tm₀
    ≡⟨ Tm-∘₀ TRUE σ γ ⟩
      TRUE {Γ = Δ} [ σ ∘₀ γ ]Tm₀
    ≡⟨ TRUE[]₀ {Γ = Δ} (σ ∘₀ γ) ⟩
      TRUE₀
    ≡⟨ sym (TRUE[]₀ {Γ = Γ} γ) ⟩
      TRUE {Γ = Γ} [ γ ]Tm₀
    ∎

  FALSE[] : {Γ Δ : GluCtx} (σ : GluSub Γ Δ)
    → (FALSE {Γ = Δ}) [ σ ]Tmᵍ ≡ FALSE {Γ = Γ}
  FALSE[] {Γ} {Δ} σ = GluTm-ext (false[]ₘ (GluSub.σ° σ)) λ γ →
      (FALSE [ σ ]Tmᵍ) [ γ ]Tm₀
    ≡⟨ Tm-∘₀ FALSE σ γ ⟩
      FALSE {Γ = Δ} [ σ ∘₀ γ ]Tm₀
    ≡⟨ FALSE[]₀ {Γ = Δ} (σ ∘₀ γ) ⟩
      FALSE₀
    ≡⟨ sym (FALSE[]₀ {Γ = Γ} γ) ⟩
      FALSE {Γ = Γ} [ γ ]Tm₀
    ∎

  IF₀ : (A : GluTy)
    → GluTm₀ BOOL → GluTm₀ A → GluTm₀ A → GluTm₀ A
  IF₀ A (b , b∙) (t , t∙) (f , f∙) .fst = ifₘ b then t else f
  IF₀ A (b , true₂ , h) (t , t∙) (f , f∙) .snd = contravariant-transport (GluTy.cA A)
    (
        ifₘ b then t else f
      ≤⟨ hom-map (λ b → ifₘ b then t else f) h ⟩
        ifₘ trueₘ then t else f
      ≤⟨ βif-trueₘ t f ⟩
        t
      ∎≤) t∙
  IF₀ A (b , false₂ , h) (t , t∙) (f , f∙) .snd = contravariant-transport (GluTy.cA A)
    (
        ifₘ b then t else f
      ≤⟨ hom-map (λ b → ifₘ b then t else f) h ⟩
        ifₘ falseₘ then t else f
      ≤⟨ βif-falseₘ t f ⟩
        f
      ∎≤) f∙

  IF : {Γ : GluCtx} {A : GluTy}
    → GluTm Γ BOOL → GluTm Γ A → GluTm Γ A → GluTm Γ A
  GluTm.M° (IF B T F) = ifₘ GluTm.M° B then GluTm.M° T else GluTm.M° F
  GluTm.M∙ (IF {A = A} B T F) γ γ∙ =
    subst (λ x → ⌞ GluTy.A∙ A x ⌟) (sym (if[]ₘ (GluTm.M° B) (GluTm.M° T) (GluTm.M° F) γ))
      (snd (IF₀ A (B [ γ , γ∙ ]Tm₀) (T [ γ , γ∙ ]Tm₀) (F [ γ , γ∙ ]Tm₀)))

  IF[]₀ : {Γ : GluCtx} {A : GluTy}
    (B : GluTm Γ BOOL) (T F : GluTm Γ A) (γ : GluSub₀ Γ)
    → (IF B T F) [ γ ]Tm₀
      ≡ IF₀ A (B [ γ ]Tm₀) (T [ γ ]Tm₀) (F [ γ ]Tm₀)
  IF[]₀ {A = A} B T F (γ , γ∙) = sym
    (ΣPathP-subst (λ x → ⌞ GluTy.A∙ A x ⌟) (sym (if[]ₘ (GluTm.M° B) (GluTm.M° T) (GluTm.M° F) γ))
      (snd (IF₀ A (B [ γ , γ∙ ]Tm₀) (T [ γ , γ∙ ]Tm₀) (F [ γ , γ∙ ]Tm₀))))

  IF[] : {Γ Δ : GluCtx} {A : GluTy}
    (B : GluTm Δ BOOL) (T F : GluTm Δ A) (σ : GluSub Γ Δ)
    → (IF B T F) [ σ ]Tmᵍ
      ≡ IF (B [ σ ]Tmᵍ) (T [ σ ]Tmᵍ) (F [ σ ]Tmᵍ)
  IF[] {A = A} B T F σ =
    GluTm-ext (if[]ₘ (GluTm.M° B) (GluTm.M° T) (GluTm.M° F) (GluSub.σ° σ)) λ γ →
        ((IF B T F) [ σ ]Tmᵍ) [ γ ]Tm₀
      ≡⟨ Tm-∘₀ (IF B T F) σ γ ⟩
        (IF B T F) [ σ ∘₀ γ ]Tm₀
      ≡⟨ IF[]₀ B T F (σ ∘₀ γ) ⟩
        IF₀ A (B [ σ ∘₀ γ ]Tm₀) (T [ σ ∘₀ γ ]Tm₀) (F [ σ ∘₀ γ ]Tm₀)
      ≡⟨ (λ i → IF₀ A (Tm-∘₀ B σ γ (~ i))
           (Tm-∘₀ T σ γ (~ i)) (Tm-∘₀ F σ γ (~ i))) ⟩
        IF₀ A ((B [ σ ]Tmᵍ) [ γ ]Tm₀) ((T [ σ ]Tmᵍ) [ γ ]Tm₀) ((F [ σ ]Tmᵍ) [ γ ]Tm₀)
      ≡⟨ sym (IF[]₀ (B [ σ ]Tmᵍ) (T [ σ ]Tmᵍ) (F [ σ ]Tmᵍ) γ) ⟩
        (IF (B [ σ ]Tmᵍ) (T [ σ ]Tmᵍ) (F [ σ ]Tmᵍ)) [ γ ]Tm₀
      ∎

  IF-preserves-β-true : {Γ : GluCtx} {A : GluTy}
    (T F : GluTm Γ A) → IF TRUE T F ≤ T
  IF-preserves-β-true {A = A} T F =
    GluTm-hom (βif-trueₘ (GluTm.M° T) (GluTm.M° F)) λ γ →
      subst (λ t → t ≤ T [ γ ]Tm₀) (sym (IF[]₀ TRUE T F γ))
        (Σ≤ _ (contravariant-lift-hom (GluTy.cA A) _ _))

  IF-preserves-β-false : {Γ : GluCtx} {A : GluTy}
    (T F : GluTm Γ A) → IF FALSE T F ≤ F
  IF-preserves-β-false {A = A} T F =
    GluTm-hom (βif-falseₘ (GluTm.M° T) (GluTm.M° F)) λ γ →
      subst (λ t → t ≤ F [ γ ]Tm₀) (sym (IF[]₀ FALSE T F γ))
        (Σ≤ _ (contravariant-lift-hom (GluTy.cA A) _ _))