open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base

open import Realisability.PCA

import Realisability.Data.Bool
import Realisability.Data.Pair
import Realisability.PCA.Sugar
module Realisability.Data.Sum {β„“} (𝔸 : PCA β„“) where
open Realisability.PCA.Sugar 𝔸
open Realisability.Data.Bool 𝔸
open Realisability.Data.Pair 𝔸

private variable
  x f g : β†― ⌞ 𝔸 ⌟

Sums in a PCAπŸ”—

`inl : ↯⁺ ⌞ 𝔸 ⌟
`inl = val ⟨ x ⟩ `pair `· `true `· x

`inr : ↯⁺ ⌞ 𝔸 ⌟
`inr = val ⟨ x ⟩ `pair `· `false `· x

`match : ↯⁺ ⌞ 𝔸 ⌟
`match = val ⟨ f ⟩ ⟨ g ⟩ ⟨ s ⟩ `fst `· s `· f `· g `· (`snd `· s)

abstract
  `inl↓₁ : ⌞ x ⌟ β†’ ⌞ `inl ⋆ x ⌟
  `inl↓₁ {x} hx = subst ⌞_⌟ (sym (abs-Ξ² _ [] (x , hx))) (`pair↓₂ (`true .snd) hx)

  `inr↓₁ : ⌞ x ⌟ β†’ ⌞ `inr ⋆ x ⌟
  `inr↓₁ {x} hx = subst ⌞_⌟ (sym (abs-Ξ² _ [] (x , hx))) (`pair↓₂ (`false .snd) hx)

  `match↓₂ : ⌞ f ⌟ β†’ ⌞ g ⌟ β†’ ⌞ `match ⋆ f ⋆ g ⌟
  `match↓₂ {f = f} {g} hf hg = subst ⌞_⌟ (sym (abs-Ξ²β‚™ [] ((g , hg) ∷ (f , hf) ∷ []))) (abs↓ _ _)

  `match-Ξ²l
    : ⌞ x ⌟ β†’ ⌞ f ⌟ β†’ ⌞ g ⌟
    β†’ `match ⋆ f ⋆ g ⋆ (`inl ⋆ x) ≑ f ⋆ x
  `match-Ξ²l {x = x} {f} {g} hx hf hg =
    `match ⋆ f ⋆ g ⋆ (`inl ⋆ x)                                        β‰‘βŸ¨ abs-Ξ²β‚™ [] ((`inl ⋆ x , `inl↓₁ hx) ∷ (g , hg) ∷ (f , hf) ∷ []) ⟩
    `fst ⋆ ⌜ `inl ⋆ x ⌝ ⋆ f ⋆ g ⋆ (`snd ⋆ ⌜ `inl ⋆ x ⌝)                β‰‘βŸ¨ ap! (abs-Ξ² _ [] (x , hx)) ⟩
    `fst ⋆ (`pair ⋆ `true ⋆ x) ⋆ f ⋆ g ⋆ (`snd ⋆ (`pair ⋆ `true ⋆ x))  β‰‘βŸ¨ apβ‚‚ (Ξ» e p β†’ e % f % g % p) (`fst-Ξ² (`true .snd) hx) (`snd-Ξ² (`true .snd) hx) ⟩
    `true ⋆ f ⋆ g ⋆ x                                                  β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ x) (`true-Ξ² hf hg) ⟩
    f ⋆ x                                                              ∎

  `match-Ξ²r
    : ⌞ x ⌟ β†’ ⌞ f ⌟ β†’ ⌞ g ⌟
    β†’ `match ⋆ f ⋆ g ⋆ (`inr ⋆ x) ≑ g ⋆ x
  `match-Ξ²r {x = x} {f} {g} hx hf hg =
    `match ⋆ f ⋆ g ⋆ (`inr ⋆ x)                                          β‰‘βŸ¨ abs-Ξ²β‚™ [] ((`inr ⋆ x , `inr↓₁ hx) ∷ (g , hg) ∷ (f , hf) ∷ []) ⟩
    `fst ⋆ ⌜ `inr ⋆ x ⌝ ⋆ f ⋆ g ⋆ (`snd ⋆ ⌜ `inr ⋆ x ⌝)                  β‰‘βŸ¨ ap! (abs-Ξ² _ [] (x , hx)) ⟩
    `fst ⋆ (`pair ⋆ `false ⋆ x) ⋆ f ⋆ g ⋆ (`snd ⋆ (`pair ⋆ `false ⋆ x))  β‰‘βŸ¨ apβ‚‚ (Ξ» e p β†’ e % f % g % p) (`fst-Ξ² (`false .snd) hx) (`snd-Ξ² (`false .snd) hx) ⟩
    `false ⋆ f ⋆ g ⋆ x                                                   β‰‘βŸ¨ ap (Ξ» e β†’ e ⋆ x) (`false-Ξ² hf hg) ⟩
    g ⋆ x                                                                ∎