module Cat.Instances.Assemblies where
private variable
: Level
β β' βA : 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
: Type β
Ob : is-set Ob
has-is-set : Ob β ββΊ πΈ
realisers : β x β β[ a β β― β πΈ β ] (a β realisers x) realised
module _ {x : Ob} where open ββΊ (realisers x) using (defined) public
open Assembly public
private variable
: Assembly πΈ β
X Y Z
instance
: Underlying (Assembly πΈ β)
Underlying-Assembly = record { β_β = Assembly.Ob }
Underlying-Assembly
: 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
hlevel-proj-asm {-# CATCHALL #-}
.hlevel-projection.get-argument _ = typeError []
hlevel-proj-asm
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 #-}
: {πΈ : PCA βA} (X : Assembly πΈ β) {x : β X β} {p q : β― β πΈ β} β [ X ] p β© x β q β‘ p β [ X ] q β© x
substβ© {x} hx p = subst (_β X .realisers x) (sym p) hx substβ© X
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
: β X β β β Y β
map : β₯ [ map ] X .realisers β’ Y .realisers β₯ tracked
private unquoteDecl eqv = declare-record-iso eqv (quote Assembly-hom)
instance
: β {n} β H-Level (Assembly-hom X Y) (2 + n)
H-Level-Assembly-hom = basic-instance 2 $ Isoβis-hlevel 2 eqv (hlevel 2)
H-Level-Assembly-hom
: β {βr} β¦ _ : Extensional (β X β β β Y β) βr β¦ β Extensional (Assembly-hom X Y) βr
Extensional-Assembly-hom = injectionβextensional! (Ξ» p β Iso.injective eqv (Ξ£-prop-path! p)) e
Extensional-Assembly-hom β¦ e β¦
: Funlike (Assembly-hom X Y) β X β Ξ» _ β β Y β
Funlike-Assembly-hom = record { _Β·_ = Assembly-hom.map }
Funlike-Assembly-hom
{-# 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
: β X β β β Y β
map : β―βΊ πΈ
realiser : (x : β X β) (a : β― β πΈ β) (ah : [ X ] a β© x) β [ Y ] realiser .fst % a β© map x
tracks
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 #-}
= record { make-assembly-hom f using (map) ; tracked = inc record { make-assembly-hom f } }
to-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.
: β β β Precategory (lsuc β β βA) (βA β β)
Assemblies .Ob = Assembly πΈ β
Assemblies β .Hom = Assembly-hom
Assemblies β .Hom-set x y = hlevel 2
Assemblies β .id = record where
Assemblies β = x
map x = inc idβ’
tracked ._β_ f g = record where
Assemblies β = f Β· (g Β· x)
map x = β¦ f .tracked ββ’ g .tracked β¦
tracked .idr f = ext Ξ» _ β refl
Assemblies β .idl f = ext Ξ» _ β refl
Assemblies β .assoc f g h = ext Ξ» _ β refl Assemblies β
Classical assembliesπ
: β {β} (X : Type β) β¦ _ : H-Level X 2 β¦ β Assembly πΈ β
β .Ob = X
β X .has-is-set = hlevel 2
β X .realisers x = record
β X { mem = def
; defined = Ξ» x β x
}
.realised x = inc (expr β¨ x β© x , absβ _ _)
β X
: Functor (Sets β) (Assemblies β)
Cofree .Fβ X = β β X β
Cofree .Fβ f = to-assembly-hom record where
Cofree = f
map = val β¨ x β© x
realiser = subst β_β (sym (abs-Ξ² _ [] (a , ha))) ha
tracks x a ha .F-id = ext Ξ» _ β refl
Cofree .F-β f g = ext Ξ» _ β refl
Cofree
: 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
Forgetβ£β = x
map x = val β¨ x β© x
realiser = subst β_β (sym (abs-Ξ² _ [] (a , X .defined ha))) (X .defined ha)
tracks x a ha
.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 Forgetβ£β
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
= case f .tracked of Ξ» where
non-constant-nabla-map f x record { realiser = (fp , fβ) ; tracks = t } β
let
= t true (`true .fst) (`true .snd)
a = t false (`true .fst) (`true .snd)
b
cases: β b b' (x : β― β πΈ β)
β [ π ] x β© b β [ π ] x β© b'
β b β b' β `true .fst β‘ `false .fst
= Ξ» where
cases β rec! Ξ» rb rb' tβ t β absurd (tβ t refl)
true true p β rec! Ξ» rb rb' _ β rb β sym rb'
true false p β rec! Ξ» rb rb' _ β rb' β sym rb
false true p β rec! Ξ» rb rb' fβ f β absurd (fβ f refl)
false false p in cases (f Β· true) (f Β· false) _ a b x