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 $a$ and $b$ is the function $$⟨i⟩\mathtt{if}i\mathtt{then}a\mathtt{else}b\text{,}$$ and the pairing function is this abstracted over $a$ and $b\text{.}$

`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  _`,_

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                       ∎