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.PCA.Sugar
module Realisability.Data.Pair {β„“} (𝔸 : PCA β„“) where
open Realisability.PCA.Sugar 𝔸
open Realisability.Data.Bool 𝔸
private variable
  a b : β†― ⌞ 𝔸 ⌟
  β„“' : Level
  V A B : Type β„“'

Pairs in a PCAπŸ”—

We define an encoding for pairs in a partial combinatory algebra in terms of the encoding of booleans in a PCA. The pairing of and is the function and the pairing function is this abstracted over and 

`pair : ↯⁺ 𝔸
`pair = val ⟨ a ⟩ ⟨ b ⟩ ⟨ i ⟩ `if i then a else b
_`,_
  : ⦃ _ : To-term V A ⦄ ⦃ _ : To-term V B ⦄
  β†’ A β†’ B β†’ TermΚ° V
a `, b = `pair `Β· a `Β· b

infixr 24 _`,_

The projection functions simply apply a pair to either `true or `false depending.

`fst : ↯⁺ 𝔸
`fst = val ⟨ p ⟩ p `· `true

`snd : ↯⁺ 𝔸
`snd = val ⟨ p ⟩ p `· `false

Our standard battery of lemmas follows: `pair is defined when applied to two arguments, and the first and second projections compute as expected.

abstract
  `pair↓₂ : ⌞ a ⌟ β†’ ⌞ b ⌟ β†’ ⌞ `pair ⋆ a ⋆ b ⌟
  `pair↓₂ {a} {b} ah bh = subst ⌞_⌟ (sym (abs-Ξ²β‚™ [] ((b , bh) ∷ (a , ah) ∷ []))) (abs↓ _ _)

  `fst-Ξ² : ⌞ a ⌟ β†’ ⌞ b ⌟ β†’ `fst ⋆ (`pair ⋆ a ⋆ b) ≑ a
  `fst-Ξ² {a} {b} ah bh =
    `fst ⋆ (`pair ⋆ a ⋆ b)  β‰‘βŸ¨ abs-Ξ² _ [] (_ , `pair↓₂ ah bh) ⟩
    `pair ⋆ a ⋆ b ⋆ `true   β‰‘βŸ¨ abs-Ξ²β‚™ [] (`true ∷ (b , bh) ∷ (a , ah) ∷ []) ⟩
    `true ⋆ a ⋆ b           β‰‘βŸ¨ `true-Ξ² ah bh ⟩
    a                       ∎

  `snd-Ξ² : ⌞ a ⌟ β†’ ⌞ b ⌟ β†’ `snd ⋆ (`pair ⋆ a ⋆ b) ≑ b
  `snd-Ξ² {a} {b} ah bh =
    `snd ⋆ (`pair ⋆ a ⋆ b)  β‰‘βŸ¨ abs-Ξ² _ [] (_ , `pair↓₂ ah bh) ⟩
    `pair ⋆ a ⋆ b ⋆ `false  β‰‘βŸ¨ abs-Ξ²β‚™ [] (`false ∷ (b , bh) ∷ (a , ah) ∷ []) ⟩
    `false ⋆ a ⋆ b          β‰‘βŸ¨ `false-Ξ² ah bh ⟩
    b                       ∎