open import Cat.Instances.Assemblies
open import Cat.Diagram.Coproduct
open import Cat.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base using ([] ; _∷_)
open import Data.Sum hiding ([_,_])

open import Realisability.PCA

import Realisability.PCA.Sugar
import Realisability.Data.Sum
import Realisability.Base

module Cat.Instances.Assemblies.Colimits {ℓA} (𝔸 : PCA ℓA) where

open Realisability.PCA.Sugar 𝔸
open Realisability.Data.Sum 𝔸
open Realisability.Base 𝔸

open is-coproduct
open Coproduct

private variable
  ℓ ℓ' : Level
  X Y Z : Assembly 𝔸 ℓ

Finite colimits of assemblies🔗

We can define the coproduct of assemblies $X,Y$ over a partial combinatory algebra $\mathbb{A}$ using our encoding of sums in a PCA. The underlying set is simply the sum type $X\uplus Y\text{,}$ and we define the realisability relation by $$\begin{array}{rlrl}\mathtt{inl}\mathsf{x}& ⊩\mathrm{inl}x& \text{iff}& \mathsf{x}⊩x\\ \mathtt{inr}\mathsf{y}& ⊩\mathrm{inr}y& \text{iff}& \mathsf{y}⊩y\text{.}\end{array}$$

_⊎Asm_ : Assembly 𝔸 ℓ → Assembly 𝔸 ℓ' → Assembly 𝔸 (ℓ ⊔ ℓ')
(X ⊎Asm Y) .Ob         = ⌞ X ⌟ ⊎ ⌞ Y ⌟
(X ⊎Asm Y) .has-is-set = hlevel 

(X ⊎Asm Y) .realisers (inl x) = record where
  mem e = elΩ (Σ[ a ∈ ↯ ⌞ 𝔸 ⌟ ] (e ≡ `inl ⋆ a × [ X ] a ⊩ x))
  def   = rec! λ _ a p → subst ⌞_⌟ (sym a) (`inl↓₁ (X .def p))

(X ⊎Asm Y) .realisers (inr x) = record where
  mem e = elΩ (Σ[ a ∈ ↯ ⌞ 𝔸 ⌟ ] (e ≡ `inr ⋆ a × [ Y ] a ⊩ x))
  def   = rec! λ _ a p → subst ⌞_⌟ (sym a) (`inr↓₁ (Y .def p))

(X ⊎Asm Y) .realised (inl x) = do
  (p , rx) ← X .realised x
  inc (`inl ⋆ p , inc (p , refl , rx))

(X ⊎Asm Y) .realised (inr x) = do
  (p , rx) ← Y .realised x
  inc (`inr ⋆ p , inc (p , refl , rx))

By construction, the constructor functions are realised by the constructor programs, i.e. `inl and `inr.

inlᴬ : Assembly-hom X (X ⊎Asm Y)
inlᴬ = to-assembly-hom record where
  map       = inl
  realiser  = `inl
  tracks ha = inc (_ , refl , ha)

inrᴬ : Assembly-hom Y (X ⊎Asm Y)
inrᴬ = to-assembly-hom record where
  map       = inr
  realiser  = `inr
  tracks ha = inc (_ , refl , ha)

Assembly-coproducts : has-coproducts (Assemblies 𝔸 ℓ)
Assembly-coproducts A B .coapex = A ⊎Asm B
Assembly-coproducts A B .ι₁ = inlᴬ
Assembly-coproducts A B .ι₂ = inrᴬ
Assembly-coproducts A B .has-is-coproduct .[_,_] {Q = Q} f g = record where
  map = λ where
    (inl a) → f · a
    (inr b) → g · b

Similarly, a pattern-matching function is tracked by a pattern matching program. Suppose $f:X\to Z$ and $g:Y\to Z$ are tracked by $\mathsf{f}$ and $\mathsf{g}\text{,}$ respectively. We want to show that $[f,g]:X\uplus Y\to Z$ is tracked by `match of $\mathsf{f}$ and $\mathsf{g}\text{.}$

  tracked = do
    ft ← f .tracked
    gt ← g .tracked
    let
      f↓ = ft .realiser .snd
      g↓ = gt .realiser .snd
    inc record where
      realiser = `match ⋆ ft ⋆ gt , `match↓₂ f↓ g↓

This is by cases on the datum we’ve applied, which lets both $[f,g]$ and the realisability relation reduce; in either case, after invoking the reduction rule for `match at a constructor, we end up with precisely with the assumptions that $f$ and $g$ are tracked.

      tracks = λ where
        {inl x} ha → □-out (Q .realisers _ .mem _ .is-tr) do
          (e , α , e⊩x) ← ha
          pure $ subst⊩ Q (ft .tracks e⊩x) $
            ap₂ _%_ refl α ∙ `match-βl (A .def e⊩x) f↓ g↓

        {inr x} ha → □-out (Q .realisers _ .mem _ .is-tr) do
          (e , α , e⊩x) ← ha
          pure $ subst⊩ Q (gt .tracks e⊩x) $
            ap₂ _%_ refl α ∙ `match-βr (B .def e⊩x) f↓ g↓

Assembly-coproducts A B .has-is-coproduct .[]∘ι₁ = ext λ _ → refl
Assembly-coproducts A B .has-is-coproduct .[]∘ι₂ = ext λ _ → refl
Assembly-coproducts A B .has-is-coproduct .unique p q = ext λ where
  (inl x) → ap map p · x
  (inr x) → ap map q · x