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.Trivial
open import Realisability.PCA

import 1Lab.Reflection as R

import Cat.Reasoning as Cat

import Realisability.Data.Bool
import Realisability.PCA.Sugar
import Realisability.Base

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.

\ Warning

The construction of assemblies over and the category works regardless of which pca we choose β€” but we only get something interesting if is nontrivial: the category over the trivial pca is the category

Therefore, when making natural-language statements about we generally assume that is nontrivial. A statement like β€œthe category is not univalent” should be read as saying β€œunivalence of implies is trivial.”

A prototypical example is the assembly of booleans, 𝟚, defined below. Its set of elements is Bool, and we fix realisers see booleans 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 over Bool, 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 which programs potentially implement them. Since we can not, for a general show that the programs and are identical, would not be a category if the choice of realiser mattered for identity of computable maps.

record Assembly-hom {𝔸 : PCA β„“A} (X : Assembly 𝔸 β„“) (Y : Assembly 𝔸 β„“') : Type (β„“A βŠ” β„“ βŠ” β„“') where
  open Realisability.Base 𝔸 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 Realisability.PCA.Sugar 𝔸 using (_⋆_)
  field
    map      : ⌞ X ⌟ β†’ ⌞ Y ⌟
    realiser : ↯⁺ 𝔸
    tracks   : (x : ⌞ X ⌟) (a : β†― ⌞ 𝔸 ⌟) (ah : [ X ] a ⊩ x) β†’ [ Y ] realiser ⋆ 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 Realisability.Base 𝔸
  open Realisability.PCA.Sugar 𝔸
  open Realisability.Data.Bool 𝔸

  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
\ Warning

Unlike most other categories constructed on the 1Lab, the category of assemblies is not univalent; see univalence of categories of assemblies.1

However, these two assemblies are still identical in the type Assembly, where we allow the identification between the sets to be nontrivial β€” their realisability relations are identical over the not equivalence β€” hence the comment above about these being non-trivial assemblies β€œover bool”.

  _ = not
  _ = `not

The assembly of booleansπŸ”—

The assembly of booleans, is the simplest example of an assembly which contains actual computability data. Its construction is entirely straightforward:

  𝟚 : Assembly 𝔸 lzero
  𝟚 .Ob          = Bool
  𝟚 .has-is-set  = hlevel 2
  𝟚 .realisers true  = singleton⁺ `true
  𝟚 .realisers false = singleton⁺ `false
  𝟚 .realised  true  = inc (`true .fst , inc refl)
  𝟚 .realised  false = inc (`false .fst , inc refl)

We define the realisability relation as a function from Bool, by cases: the only option for realising the boolean true is with the `true program, and similarly the false boolean is realised by the `false program. Both elements have those respective programs as their realisers.

Indiscrete assembliesπŸ”—

However, the assembly of booleans is not the only assembly we can construct on the type of booleans. As mentioned above, we could also have inverted which program realises each boolean; but this is still an assembly with nontrivial computability data. Now, we show that the β€œambient” world of sets and functions embeds fully faithful into the category of assemblies over any pca

This is, perhaps, a bit surprising: maps of assemblies are computable by definition, but arbitrary functions between sets need not be! The catch is that, when equipping a set with the structure of an assembly, we get to choose which programs compute each elements; and, above, we have made a sensible choice. But we can always make an adversarial choice, letting every program at all realise any element.

Terminology

We denote the indiscrete assembly on a set as following the literature. Note however that Bauer (2022) refers to these as constant assemblies, while de Jong (2024) does not assign them a name but merely singles them out as embedding classical logic in 

  βˆ‡ : βˆ€ {β„“} (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↓ _ _)

The important thing to know about these is that any function of sets extends to a computable map of assemblies β€” this is because the only requirement for is that is defined, and assemblies are defined so that if then is defined.

Following the general logic of adjoint functors, this means that is a functor for any at all β€” and moreover that is a right adjoint to the functor which projects the underlying set of each assembly. 
  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 indiscrete assemblies are generally poor as domains for computable functions, since a realiser for would have to choose realisers for given no information about Indeed, we can show that if there are non-constant maps then is trivial.

  non-constant-nabla-map
    : (f : Assembly-hom (βˆ‡ Bool) 𝟚)
    β†’ f Β· true β‰  f Β· false
    β†’ is-trivial-pca 𝔸
  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
module Asm {β„“A β„“} {𝔸 : PCA β„“A} = Cat (Assemblies 𝔸 β„“)

  1. This is essentially because of of assemblies such as 𝟚 and its β€œflipped” counterpart, described above. The identity map is a computable isomorphism between them, realised by the `not program, which does not extend to a path (unless is trivial).β†©οΈŽ

References