open import 1Lab.Reflection.HLevel

open import Cat.Functor.Adjoint
open import Cat.Prelude

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

open import Realisability.PCA

import 1Lab.Reflection as R

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

open R hiding (def ; absurd)
open Functor
open _=>_
open _⊣_
module Cat.Instances.Assemblies where
private variable
  β„“ β„“' β„“A : Level
  𝔸 : PCA β„“A

Assemblies over a PCAπŸ”—

When working over a partial combinatory algebra it’s often the case that we’re interested in programs as concrete implementations of some mathematical datum For example, we can implement the successor function on natural numbers to be representing a numeral as a Church numeral, taking the defining property of to be that if we have some iterable process starting at then the iteration is applied to the iteration; But we could just as well implement representing a numeral as a Curry numeral, a pair containing the information of whether the number is zero and its predecessor (if any). These implementations are extensionally identical, in that they both denote the same actual natural number, but for a concrete pca they might genuinely be different β€” we could imagine measuring the time complexity of the predecessor function, which is for Curry numbers and for Church numbers. Therefore, if we are to investigate the computational content of constructive mathematics, we need a way to track the connection between the mathematical elements and the programs which denote them.

An assembly over a pca is a set equipped with a propositional relation between programs and elements when this holds, we say realises Moreover, for every we require that there be at least one which realises it.

A prototypical example is the assembly of booleans, 𝟚, defined below. Its set of elements is Bool, and we fix realisers see pairs in a PCA for the details of the construction. This is not the only possible choice: we could, for example, invert the realisers, and say that the value true is implemented by the program (and vice-versa). This results in a genuinely different assembly, though with the same denotational data.

record Assembly (𝔸 : PCA β„“A) β„“ : Type (lsuc β„“ βŠ” β„“A) where
  no-eta-equality
  field
    Ob         : Type β„“
    has-is-set : is-set Ob
    realisers  : Ob β†’ ℙ⁺ 𝔸
    realised   : βˆ€ x β†’ βˆƒ[ a ∈ β†― ⌞ 𝔸 ⌟ ] (a ∈ realisers x)
  module _ {x : Ob} where open ℙ⁺ (realisers x) using (defined) public

open Assembly public

private variable
  X Y Z : Assembly 𝔸 β„“

instance
  Underlying-Assembly : Underlying (Assembly 𝔸 β„“)
  Underlying-Assembly = record { ⌞_⌟ = Assembly.Ob }

  hlevel-proj-asm : hlevel-projection (quote Assembly.Ob)
  hlevel-proj-asm .hlevel-projection.has-level = quote Assembly.has-is-set
  hlevel-proj-asm .hlevel-projection.get-level _ = pure (quoteTerm (suc (suc zero)))
  hlevel-proj-asm .hlevel-projection.get-argument (_ ∷ _ ∷ _ ∷ c v∷ []) = pure c
  hlevel-proj-asm .hlevel-projection.get-argument (_ ∷ c v∷ []) = pure c
  {-# CATCHALL #-}
  hlevel-proj-asm .hlevel-projection.get-argument _ = typeError []

module _ (X : Assembly 𝔸 β„“) (a : β†― ⌞ 𝔸 ⌟) (x : ⌞ X ⌟) where open Ξ© (X .realisers x .mem a) renaming (∣_∣ to [_]_⊩_) public

-- This module can't be parametrised so this display form can fire
-- (otherwise it gets closed over pattern variables that aren't solvable
-- from looking at the expression, like the level and the PCA):
{-# DISPLAY realisers X x .ℙ⁺.mem a = [ X ] a ⊩ x #-}

subst⊩ : {𝔸 : PCA β„“A} (X : Assembly 𝔸 β„“) {x : ⌞ X ⌟} {p q : β†― ⌞ 𝔸 ⌟} β†’ [ X ] p ⊩ x β†’ q ≑ p β†’ [ X ] q ⊩ x
subst⊩ X {x} hx p = subst (_∈ X .realisers x) (sym p) hx

To understand the difference β€” and similarity β€” between the ordinary assembly of booleans and the swapped booleans, we define a morphism of assemblies to be a function satisfying the property that there exists a program which sends realisers of to realisers of Note the force of the propositional truncation in this definition: maps of assemblies are identical when they have the same underlying function, regardless of what program implements them.

record Assembly-hom {𝔸 : PCA β„“A} (X : Assembly 𝔸 β„“) (Y : Assembly 𝔸 β„“') : Type (β„“A βŠ” β„“ βŠ” β„“') where
  open Logic 𝔸 using ([_]_⊒_)

  field
    map     : ⌞ X ⌟ β†’ ⌞ Y ⌟
    tracked : βˆ₯ [ map ] X .realisers ⊒ Y .realisers βˆ₯
private unquoteDecl eqv = declare-record-iso eqv (quote Assembly-hom)

instance
  H-Level-Assembly-hom : βˆ€ {n} β†’ H-Level (Assembly-hom X Y) (2 + n)
  H-Level-Assembly-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)

  Extensional-Assembly-hom : βˆ€ {β„“r} ⦃ _ : Extensional (⌞ X ⌟ β†’ ⌞ Y ⌟) β„“r ⦄ β†’ Extensional (Assembly-hom X Y) β„“r
  Extensional-Assembly-hom ⦃ e ⦄ = injectionβ†’extensional! (Ξ» p β†’ Iso.injective eqv (Ξ£-prop-path! p)) e

  Funlike-Assembly-hom : Funlike (Assembly-hom X Y) ⌞ X ⌟ Ξ» _ β†’ ⌞ Y ⌟
  Funlike-Assembly-hom = record { _Β·_ = Assembly-hom.map }

{-# DISPLAY Assembly-hom.map f x = f Β· x #-}

-- Helper record for constructing an assembly map when the realiser is
-- known/does not depend on other truncated data; the 'tracks' field has
-- all visible arguments to work with `record where` syntax.

record make-assembly-hom {𝔸 : PCA β„“A} (X : Assembly 𝔸 β„“) (Y : Assembly 𝔸 β„“') : Type (β„“A βŠ” β„“ βŠ” β„“') where
  open PCA 𝔸 using (_%_)
  field
    map      : ⌞ X ⌟ β†’ ⌞ Y ⌟
    realiser : ↯⁺ 𝔸
    tracks   : (x : ⌞ X ⌟) (a : β†― ⌞ 𝔸 ⌟) (ah : [ X ] a ⊩ x) β†’ [ Y ] realiser .fst % a ⊩ map x

open Assembly-hom public

to-assembly-hom
  : βˆ€ {𝔸 : PCA β„“A} {X : Assembly 𝔸 β„“} {Y : Assembly 𝔸 β„“'}
  β†’ make-assembly-hom X Y
  β†’ Assembly-hom X Y
{-# INLINE to-assembly-hom #-}

to-assembly-hom f = record { make-assembly-hom f using (map) ; tracked = inc record { make-assembly-hom f } }

module _ (𝔸 : PCA β„“A) where
  open Logic 𝔸
  open Sugar 𝔸
  open Pair 𝔸

  open Assembly-hom
  open Precategory

This consideration is necessary for assemblies and assembly morphisms to be a category: in an arbitrary PCA composition of programs need not be unital or associative.

  Assemblies : βˆ€ β„“ β†’ Precategory (lsuc β„“ βŠ” β„“A) (β„“A βŠ” β„“)
  Assemblies β„“ .Ob      = Assembly 𝔸 β„“
  Assemblies β„“ .Hom     = Assembly-hom
  Assemblies β„“ .Hom-set x y = hlevel 2
  Assemblies β„“ .id      = record where
    map x   = x
    tracked = inc id⊒
  Assemblies β„“ ._∘_ f g = record where
    map x   = f Β· (g Β· x)
    tracked = ⦇ f .tracked ∘⊒ g .tracked ⦈
  Assemblies β„“ .idr   f     = ext Ξ» _ β†’ refl
  Assemblies β„“ .idl   f     = ext Ξ» _ β†’ refl
  Assemblies β„“ .assoc f g h = ext Ξ» _ β†’ refl

Classical assembliesπŸ”—

  βˆ‡ : βˆ€ {β„“} (X : Type β„“) ⦃ _ : H-Level X 2 ⦄ β†’ Assembly 𝔸 β„“
  βˆ‡ X .Ob          = X
  βˆ‡ X .has-is-set  = hlevel 2
  βˆ‡ X .realisers x = record
    { mem     = def
    ; defined = Ξ» x β†’ x
    }
  βˆ‡ X .realised x = inc (expr ⟨ x ⟩ x , abs↓ _ _)

  Cofree : Functor (Sets β„“) (Assemblies β„“)
  Cofree .Fβ‚€ X = βˆ‡ ⌞ X ⌟
  Cofree .F₁ f = to-assembly-hom record where
    map           = f
    realiser      = val ⟨ x ⟩ x
    tracks x a ha = subst ⌞_⌟ (sym (abs-β _ [] (a , ha))) ha
  Cofree .F-id    = ext Ξ» _ β†’ refl
  Cofree .F-∘ f g = ext Ξ» _ β†’ refl

  Forget : Functor (Assemblies β„“) (Sets β„“)
  Forget .Fβ‚€ X    = el! ⌞ X ⌟
  Forget .F₁ f    = f Β·_
  Forget .F-id    = refl
  Forget .F-∘ f g = refl

  ForgetβŠ£βˆ‡ : Forget {β„“} ⊣ Cofree
  ForgetβŠ£βˆ‡ .unit .Ξ· X = to-assembly-hom record where
    map x         = x
    realiser      = val ⟨ x ⟩ x
    tracks x a ha = subst ⌞_⌟ (sym (abs-β _ [] (a , X .defined ha))) (X .defined ha)

  ForgetβŠ£βˆ‡ .unit .is-natural x y f = ext Ξ» _ β†’ refl
  ForgetβŠ£βˆ‡ .counit .Ξ· X a = a
  ForgetβŠ£βˆ‡ .counit .is-natural x y f = refl
  ForgetβŠ£βˆ‡ .zig = refl
  ForgetβŠ£βˆ‡ .zag = ext Ξ» _ β†’ refl

The assembly of booleansπŸ”—

  𝟚 : Assembly 𝔸 lzero
  𝟚 .Ob = Bool
  𝟚 .has-is-set  = hlevel 2
  𝟚 .realisers true  = record
    { mem     = Ξ» x β†’ elΞ© (`true .fst ≑ x)
    ; defined = rec! Ξ» p β†’ subst ⌞_⌟ p (`true .snd)
    }
  𝟚 .realisers false = record
    { mem     = Ξ» x β†’ elΞ© (`false .fst ≑ x)
    ; defined = rec! Ξ» p β†’ subst ⌞_⌟ p (`false .snd)
    }
  𝟚 .realised true  = inc (`true .fst , inc refl)
  𝟚 .realised false = inc (`false .fst , inc refl)
  non-constant-nabla-map
    : (f : Assembly-hom (βˆ‡ Bool) 𝟚)
    β†’ f Β· true β‰  f Β· false
    β†’ `true .fst ≑ `false .fst
  non-constant-nabla-map f x = case f .tracked of Ξ» where
    record { realiser = (fp , f↓) ; tracks = t } β†’
      let
        a = t true  (`true .fst) (`true .snd)
        b = t false (`true .fst) (`true .snd)

        cases
          : βˆ€ b b' (x : β†― ⌞ 𝔸 ⌟)
          β†’ [ 𝟚 ] x ⊩ b β†’ [ 𝟚 ] x ⊩ b'
          β†’ b β‰  b' β†’ `true .fst ≑ `false .fst
        cases = Ξ» where
          true true   p → rec! λ rb rb' t≠t → absurd (t≠t refl)
          true false  p β†’ rec! Ξ» rb rb' _   β†’ rb βˆ™ sym rb'
          false true  p β†’ rec! Ξ» rb rb' _   β†’ rb' βˆ™ sym rb
          false false p → rec! λ rb rb' f≠f → absurd (f≠f refl)
      in cases (f Β· true) (f Β· false) _ a b x