open import Cat.Diagram.Limit.Finite
open import Cat.Instances.Assemblies
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Cartesian
open import Cat.Prelude

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

open import Realisability.PCA

import Realisability.Data.Pair
import Realisability.PCA.Sugar
import Realisability.Base

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

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

open is-equaliser
open is-product
open Equaliser
open Terminal
open Product

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

Finite limits of assemblies🔗

We can define finite limits in a category of assemblies over a partial combinatory algebra $A$ using the encoding of pairs in a PCA.

The product of a pair of assemblies has underlying set the product of their underlying sets, and the realisability relation $e ⊩ (x, y)$ is generated by $pair x y ⊩ (x, y)$ whenever $x ⊩ x$ and $y ⊩ y .$

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

(X ×Asm Y) .realisers (x , y) = record where
  mem p = elΩ $
    Σ[ a ∈ ↯ ⌞ 𝔸 ⌟ ] Σ[ b ∈ ↯ ⌞ 𝔸 ⌟ ]
      p ≡ `pair ⋆ a ⋆ b × [ X ] a ⊩ x × [ Y ] b ⊩ y

  def : {a : ↯ ⌞ 𝔸 ⌟} → a ∈ mem → ⌞ a ⌟
  def = rec! λ a b p rx ry →
    subst ⌞_⌟ (sym p) (`pair↓₂ (X .def rx) (Y .def ry))

Of course, every pair is realised because both the first and second components have realisers.

(X ×Asm Y) .realised (x , y) = do
  pxrx ← X .realised x
  pyry ← Y .realised y
  let
    (px , rx) = pxrx
    (py , ry) = pyry
  inc (`pair ⋆ px ⋆ py , inc (px , py , refl , rx , ry))

The first projection, second projection, and pairing maps are realised by their respective programs, `fst, `snd and `pair. Since equality of assembly maps is at the level of the underlying set-functions, these satisfy the universal property by trivial computations.

π₁Asm : Assembly-hom (X ×Asm Y) X
π₁Asm {X = X} {Y = Y} = to-assembly-hom record where
  map (x , _)    = x
  realiser       = `fst
  tracks {a = a} = elim! λ p q α rx ry → subst⊩ X rx $
    `fst ⋆ a                ≡⟨ ap (`fst ⋆_) α ⟩≡
    `fst ⋆ (`pair ⋆ p ⋆ q)  ≡⟨ `fst-β (X .def rx) (Y .def ry) ⟩≡
    p                       ∎

π₂Asm : Assembly-hom (X ×Asm Y) Y
π₂Asm {X = X} {Y = Y} = to-assembly-hom record where
  map (_ , x)    = x
  realiser       = `snd
  tracks {a = a} = elim! λ p q α rx ry → subst⊩ Y ry $
    ap (`snd ⋆_) α ∙ `snd-β (X .def rx) (Y .def ry)

⟨_,_⟩Asm : Assembly-hom Z X → Assembly-hom Z Y → Assembly-hom Z (X ×Asm Y)
⟨_,_⟩Asm {Z = Z} f g = record where
  map x = f · x , g · x

  tracked = do
    rf ← f .tracked
    rg ← g .tracked
    inc record where
      realiser = val ⟨ x ⟩ (rf `· x `, rg `· x)

      tracks {a = a} qx = inc
        ( rf ⋆ a , rg ⋆ a , abs-β _ _ (a , Z .def qx)
        , rf .tracks qx , rg .tracks qx )

Assemblies-products : has-products (Assemblies 𝔸 ℓ)
Assemblies-products X Y .apex = X ×Asm Y
Assemblies-products X Y .π₁ = π₁Asm
Assemblies-products X Y .π₂ = π₂Asm
Assemblies-products X Y .has-is-product .⟨_,_⟩ f g = ⟨ f , g ⟩Asm
Assemblies-products X Y .has-is-product .π₁∘⟨⟩ = ext λ _ → refl
Assemblies-products X Y .has-is-product .π₂∘⟨⟩ = ext λ _ → refl
Assemblies-products X Y .has-is-product .unique p q = ext λ a → p ·ₚ a ,ₚ q ·ₚ a

The terminal assembly🔗

The terminal assembly has the unit type as its underlying set, and we let any $x ⊩ tt .$ Alternatively, we could have defined the terminal assembly so an arbitrary choice of element $x : A$ realises the point, and the terminating map !Asm would be tracked by the constant function with value $x .$

⊤Asm : Assembly 𝔸 ℓ
⊤Asm .Ob          = Lift _ ⊤
⊤Asm .has-is-set  = hlevel 2
⊤Asm .realisers _ = defineds
⊤Asm .realised  _ = inc (val ⟨ x ⟩ x)

!Asm : Assembly-hom X (⊤Asm {ℓ})
!Asm {X = X} = to-assembly-hom record where
  map    _  = lift tt
  realiser  = val ⟨ x ⟩ x
  tracks ha = subst ⌞_⌟ (sym (abs-β _ [] (_ , X .def ha))) (X .def ha)

Assemblies-terminal : Terminal (Assemblies 𝔸 ℓ)
Assemblies-terminal .top = ⊤Asm
Assemblies-terminal .has⊤ X .centre  = !Asm
Assemblies-terminal .has⊤ X .paths x = ext λ _ → refl

Equalisers🔗

The equaliser of a pair of assembly maps $f, g : X \to Y$ has underlying set the equaliser of $f$ and $g,$ i.e. the type $x : X \sum f (x) = g (x);$ the realisability relation is directly inherited from the domain, and the equalising map is (at the level of types) the first projection function, realised by the identity program.

Equ-asm : (f g : Assembly-hom X Y) → Assembly 𝔸 _
Equ-asm {X = X} f g .Ob = Σ[ x ∈ X ] (f · x ≡ g · x)
Equ-asm {X = X} f g .has-is-set = hlevel 2
Equ-asm {X = X} f g .realisers (x , _) = X .realisers x
Equ-asm {X = X} f g .realised  (x , _) = X .realised x

Assemblies-equalisers : has-equalisers (Assemblies 𝔸 ℓ)
Assemblies-equalisers f g .apex = Equ-asm f g
Assemblies-equalisers {a = A} f g .equ = to-assembly-hom record where
  map (x , _) = x
  realiser    = val ⟨ x ⟩ x
  tracks ha   = subst⊩ A ha (abs-β _ [] (_ , A .def ha))
Assemblies-equalisers f g .has-is-eq .equal = ext λ x p → p

The universal map $u : W \to Eq (f, g)$ into the equaliser given by some $e : W \to X$ differs from $e$ only at the level of sets, so any realiser of $e$ is also a realiser of $u .$

Assemblies-equalisers f g .has-is-eq .universal {e' = e'} p =
  record where
    map x  = e' · x , ap map p · x
    tracked = do
      et ← e' .tracked
      inc record { [_]_⊢_ et }

Assemblies-equalisers f g .has-is-eq .factors  = ext λ _ → refl
Assemblies-equalisers f g .has-is-eq .unique p = ext λ a → Σ-prop-path! (p ·ₚ a)

Assemblies-finite-limits : Finitely-complete (Assemblies 𝔸 ℓ)
Assemblies-finite-limits = with-equalisers _
  Assemblies-terminal
  Assemblies-products
  Assemblies-equalisers

Assemblies-cartesian : Cartesian-category (Assemblies 𝔸 ℓ)
Assemblies-cartesian = record { Finitely-complete Assemblies-finite-limits }