more prose on assemblies

Author: plt-amy

src/Cat/Instances/Assemblies.lagda.md

@@ -8,13 +8,16 @@ 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 Realisability.Data.Pair as Pair
-import Realisability.PCA.Sugar as Sugar
-import Realisability.Base as Logic
+import Cat.Reasoning as Cat
+
+import Realisability.Data.Bool
+import Realisability.PCA.Sugar
+import Realisability.Base
 
 open R hiding (def ; absurd)
 open Functor
@@ -71,6 +74,20 @@ $\tt{p}$ **realises** $x$. Moreover, for every $x : X$, we require that
 there be at least one $\tt{p}$ which realises it.
 :::
 
+::: warning
+The construction of assemblies over $\bA$, and the category
+$\thecat{Asm}(\bA)$, works regardless of *which* pca $\bA$ we choose ---
+but we only get something *interesting* if $\bA$ is [[nontrivial|trivial
+pca]]: the category $\thecat{Asm}(*)$ over the trivial pca is the
+category $\Sets$.
+
+Therefore, when making natural-language statements about
+$\thecat{Asm}(\bA)$, we generally assume that $\bA$ is nontrivial. A
+statement like "the category $\thecat{Asm}(\bA)$ is not
+[[univalent|univalent category]]" should be read as saying "univalence
+of $\thecat{Asm}(\bA)$ implies $\bA$ is trivial."
+:::
+
 A prototypical example is the assembly of booleans, `𝟚`{.Agda}, defined
 [below](#the-assembly-of-booleans). Its set of elements is
 `Bool`{.Agda}, and we fix realisers
@@ -80,11 +97,11 @@ $$
 \left(\langle x \rangle \langle y \rangle\ y\right) \Vdash&\ \rm{false;}
 \end{align*}
 $$
-see [[pairs in a PCA]] for the details of the construction. This is not
+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`{.Agda} is implemented by the *program*
 $\tt{false}$ (and vice-versa). This results in a genuinely different
-assembly, though with the same denotational data.
+assembly over `Bool`{.Agda}, though with the same denotational data.
 
 ```agda
 record Assembly (𝔸 : PCA ℓA) ℓ : Type (lsuc ℓ ⊔ ℓA) where
@@ -117,14 +134,17 @@ instance
   {-# 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
+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⊩
+  : {𝔸 : 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
 ```
 -->
@@ -134,13 +154,22 @@ assembly of booleans and the swapped booleans, we define a morphism of
 assemblies $(X, \Vdash_X) \to (Y, \Vdash_Y)$ to be a function $f : X \to
 Y$ satisfying the [[*property*|propositional truncation]] that there
 exists a program $\tt{f} : \bA$ which sends realisers of $x : X$ to
-realisers of $f(x) : Y$. 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.
+realisers of $f(x) : Y$.
+
+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 $\bA$, show that the programs
+$\mathtt{f}$ and
+$$
+\langle a \rangle\ f\ a
+$$
+are identical, $\thecat{Asm}(\bA)$ would not be a category if the choice
+of realiser mattered for identity of computable maps.
 
 ```agda
 record Assembly-hom {𝔸 : PCA ℓA} (X : Assembly 𝔸 ℓ) (Y : Assembly 𝔸 ℓ') : Type (ℓA ⊔ ℓ ⊔ ℓ') where
-  open Logic 𝔸 using ([_]_⊢_)
+  open Realisability.Base 𝔸 using ([_]_⊢_)
 
   field
     map     : ⌞ X ⌟ → ⌞ Y ⌟
@@ -155,7 +184,9 @@ 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
+    : ∀ {ℓ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 ⌟
@@ -168,11 +199,11 @@ instance
 -- 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 (_%_)
+  open Realisability.PCA.Sugar 𝔸 using (_⋆_)
   field
     map      : ⌞ X ⌟ → ⌞ Y ⌟
     realiser : ↯⁺ 𝔸
-    tracks   : (x : ⌞ X ⌟) (a : ↯ ⌞ 𝔸 ⌟) (ah : [ X ] a ⊩ x) → [ Y ] realiser .fst % a ⊩ map x
+    tracks   : (x : ⌞ X ⌟) (a : ↯ ⌞ 𝔸 ⌟) (ah : [ X ] a ⊩ x) → [ Y ] realiser ⋆ a ⊩ map x
 
 open Assembly-hom public
 
@@ -185,17 +216,17 @@ 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 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 $\bA$, composition of programs need
+be a category: in an arbitrary pca $\bA$, composition of programs need
 not be unital or associative.
 
 ```agda
@@ -214,7 +245,74 @@ not be unital or associative.
   Assemblies ℓ .assoc f g h = ext λ _ → refl
 ```
 
-## Classical assemblies
+::: warning
+Unlike most other categories constructed on the 1Lab, the category of
+assemblies is not [[univalent|univalent category]]. This is essentially
+*because* of the existence of assemblies such as `𝟚`{.Agda} and its
+"flipped" counterpart, described above: the identity map is a computable
+isomorphism between them, realised by the `` `not ``{.Agda} program, but
+there is no path in `Assembly`{.Agda} between them with first component
+projecting to the identity map.
+:::
+
+However, these two assemblies *are* still identical in the type
+`Assembly`{.Agda}, where we allow the identification between the sets to
+be nontrivial --- their realisability relations are identical over the
+`not`{.Agda} equivalence --- hence the comment above about these being
+non-trivial assemblies "over bool".
+
+<!--
+```agda
+  _ = not
+  _ = `not
+```
+-->
+
+## The assembly of booleans
+
+The assembly of booleans, $\tt{2}$, is the simplest example of an
+assembly which contains actual computability data. Its construction is
+entirely straightforward:
+
+```agda
+  𝟚 : 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`{.Agda},
+by cases: the only option for realising the boolean `true`{.Agda} is
+with the `` `true ``{.Agda} program, and similarly the `false`{.Agda}
+boolean is realised by the `` `false ``{.Agda} 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|fully
+faithful functor]] into the category of assemblies over any pca $\bA$.
+
+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 $X$ as $\nabla X$,
+following the literature. Note however that Bauer
+[-@Bauer:Realisability] refers to these as *constant assemblies*, while
+de Jong [-@deJong:Realisability] does not assign them a name but merely
+singles them out as embedding classical logic in $\thecat{Asm}(\bA)$.
+:::
 
 ```agda
   ∇ : ∀ {ℓ} (X : Type ℓ) ⦃ _ : H-Level X 2 ⦄ → Assembly 𝔸 ℓ
@@ -225,7 +323,22 @@ not be unital or associative.
     ; defined = λ x → x
     }
   ∇ X .realised x = inc (expr ⟨ x ⟩ x , abs↓ _ _)
+```
+
+The important thing to know about these is that any function of sets $X
+\to Y$ extends to a computable map of assemblies $(X, \Vdash) \to \nabla
+Y$ --- this is because the only requirement for $e \Vdash_{\nabla Y} f
+x$ is that $e$ is defined, and assemblies are defined so that if $e
+\Vdash_X x$ then $e$ is defined.
 
+<details>
+<summary>Following the general logic of [[adjoint functors]], this means
+that $\nabla (-)$ is a functor $\Sets \to \thecat{Asm}(\bA)$, for any
+$\bA$ at all --- and moreover that $\nabla$ is a [[right adjoint]] to
+the functor $\Gamma : \thecat{Asm}(\bA) \to \Sets$ which projects the
+underlying set of each assembly.</summary>
+
+```agda
   Cofree : Functor (Sets ℓ) (Assemblies ℓ)
   Cofree .F₀ X = ∇ ⌞ X ⌟
   Cofree .F₁ f = to-assembly-hom record where
@@ -254,29 +367,19 @@ not be unital or associative.
   Forget⊣∇ .zag = ext λ _ → refl
 ```
 
-## The assembly of booleans
+</details>
 
-```agda
-  𝟚 : 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)
-```
+The indiscrete assemblies $\nabla X$ are generally poor as *domains* for
+computable functions, since a realiser for $f : \nabla X \to (Y,
+\Vdash)$ would have to choose realisers for $f(x)$ given no information
+about $x$. Indeed, we can show that if there are non-constant maps
+$\nabla \{0, 1\} \to \tt{2}$, then $\bA$ is [[trivial|trivial pca]].
 
 ```agda
   non-constant-nabla-map
     : (f : Assembly-hom (∇ Bool) 𝟚)
     → f · true ≠ f · false
-    → `true .fst ≡ `false .fst
+    → is-trivial-pca 𝔸
   non-constant-nabla-map f x = case f .tracked of λ where
     record { realiser = (fp , f↓) ; tracks = t } →
       let
@@ -294,3 +397,9 @@ not be unital or associative.
           false false p → rec! λ rb rb' f≠f → absurd (f≠f refl)
       in cases (f · true) (f · false) _ a b x
 ```
+
+<!--
+```agda
+module Asm {ℓA ℓ} {𝔸 : PCA ℓA} = Cat (Assemblies 𝔸 ℓ)
+```
+-->

src/Data/Partial/Base.lagda.md

@@ -210,6 +210,14 @@ part-ap f x .elt (pf , px) = f .elt pf (x .elt px)
 is-always : {A : Type ℓ} (a : ↯ A) (x : ⌞ a ⌟) → a ≡ always (a .elt x)
 is-always a x = part-ext (λ _ → tt) (λ z → x) λ _ _ → ↯-indep a
 
+always-injective : {A : Type ℓ} {x y : A} → always x ≡ always y → x ≡ y
+always-injective p = ap₂ unalways p q where
+  unalways : (x : ↯ A) → ⌞ x ⌟ → A
+  unalways = elt
+
+  q : PathP (λ i → ⌞ p i ⌟) tt tt
+  q = is-prop→pathp (λ i → p i .def .is-tr) tt tt
+
 instance
   ↯-Map : Map (eff ↯)
   ↯-Map .Map.map = part-map

src/Data/Partial/Total.lagda.md

@@ -109,3 +109,9 @@ from-total-predicate-is-equiv = is-iso→is-equiv λ where
   .rinv P → ext λ a → Ω-ua (rec! (λ ha → subst (_∈ P) (sym (is-always a ha)))) λ pa → P .defined pa , subst (_∈ P) (is-always a _) pa
   .linv P → ext λ a → Ω-ua snd (tt ,_)
 ```
+
+```agda
+singleton⁺ : ↯⁺ A → ℙ⁺ A
+singleton⁺ x .mem y = elΩ (x .fst ≡ y)
+singleton⁺ x .defined = rec! λ p → subst ⌞_⌟ p (x .snd)
+```

src/Realisability/Data/Bool.lagda.md

@@ -0,0 +1,57 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Partial.Total
+open import Data.Partial.Base
+open import Data.Vec.Base
+
+open import Realisability.PCA
+
+import Realisability.PCA.Sugar as S
+```
+-->
+
+```agda
+module Realisability.Data.Bool {ℓ} (𝔸@(A , _) : PCA ℓ) where
+```
+
+<!--
+```agda
+open S 𝔸
+private variable
+  a b : ↯ ⌞ 𝔸 ⌟
+```
+-->
+
+# Booleans in a PCA {defines="booleans-in-a-pca"}
+
+```agda
+`true : ↯⁺ 𝔸
+`true = val ⟨ x ⟩ ⟨ y ⟩ x
+
+`false : ↯⁺ 𝔸
+`false = val ⟨ x ⟩ ⟨ y ⟩ y
+
+`not : ↯⁺ A
+`not = val ⟨ x ⟩ x `· `false `· `true
+
+abstract
+  `true↓₁ : ⌞ a ⌟ → ⌞ `true ⋆ a ⌟
+  `true↓₁ x = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , x) ∷ []))) (abs↓ _ _)
+
+  `false↓₁ : ⌞ a ⌟ → ⌞ `false .fst % a ⌟
+  `false↓₁ ah = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , ah) ∷ []))) (abs↓ _ _)
+
+  `false-β : ⌞ a ⌟ → ⌞ b ⌟ → `false ⋆ a ⋆ b ≡ b
+  `false-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])
+
+  `true-β : ⌞ a ⌟ → ⌞ b ⌟ → `true ⋆ a ⋆ b ≡ a
+  `true-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])
+
+  `not-βt : `not ⋆ `true ≡ `false .fst
+  `not-βt = abs-β _ [] `true ∙ abs-βₙ [] (`true ∷ `false ∷ [])
+
+  `not-βf : `not ⋆ `false ≡ `true .fst
+  `not-βf = abs-β _ [] `false ∙ abs-βₙ [] (`true ∷ `false ∷ [])
+```

src/Realisability/Data/Nat.lagda.md

@@ -9,6 +9,7 @@ open import Data.Vec.Base
 open import Realisability.PCA
 
 import Realisability.PCA.Fixpoint
+import Realisability.Data.Bool
 import Realisability.Data.Pair
 import Realisability.PCA.Sugar
 ```
@@ -23,6 +24,7 @@ module Realisability.Data.Nat {ℓ} (𝔸 : PCA ℓ) where
 open Realisability.PCA.Fixpoint 𝔸
 open Realisability.PCA.Sugar 𝔸
 open Realisability.Data.Pair 𝔸
+open Realisability.Data.Bool 𝔸
 ```
 -->