module Data.Partial.Total where

Total partial elements🔗

An important property of the partial elements is that if is defined, then it is necessarily the inclusion of a unique total value However, when formalising, we have to contend with the following infelicity: if we start with a partial element extract an underlying value by proving that it is defined, and then subsequently weaken back to a partial element, we do not definitionally end up back with

This turns into a compound annoyance when we’re dealing with partial operators, like those of a partial combinatory algebra, since we want to ergonomically build complex expressions— which entails ‘lifting’ a partial operator to a binary operation on using the monadic structure of but the properties that control these operators only apply when the domains are actually defined. We would thus have to insert tons of mediating identifications between a (defined) partial element and the inclusion of its underlying value.

A better approach from the perspective of formalisation is thus to delay projecting the underlying value as long as possible. Instead, we prefer to work with partial elements and carry the proofs that they are defined ‘off to the side’. To make this precise, we define a type of defined partial elements of which, extensionally, is just again; but which, intensionally, lets us definitionally recover a partial after proving that it is defined, by merely projecting out the underlying partial element.

↯⁺ :  {} {X : Type }  u : Underlying X   X  Type _
↯⁺ A = Σ[ a    A  ]  a 

It’s actually very easy to prove that this type is equivalent to which at a glance might call its utility into question — but it will be extensively used in the development of realisability.

from-total : ↯⁺ A  A
from-total (a , ha) = a .elt ha

from-total-is-equiv : is-equiv (from-total {A = A})
from-total-is-equiv = is-iso→is-equiv record where
  from x       = pure x
  rinv _       = refl
  linv (x , a) = Σ-prop-path! (sym (is-always x a))

Total power sets🔗

We can perform a similar replacement to the power set pairing a predicate on partial elements with a proof that every member of is defined. Again, this is equivalent to but it lets us talk directly about the membership of partial elements in even those which are not a priori known to be defined.

  record ℙ⁺ (A : Type ) : Type  where
    field
      mem :  A  Ω
      def :  {a}   mem a    a 

Of course, if we have a predicate we can extend it to a defined on partial elements by defining to mean “ is defined and the projection of onto belongs to ”. By construction, every member of is defined.

from-total-predicate :  A  ℙ⁺ A
from-total-predicate P .mem x = el (Σ[ hx  x ] x .elt hx  P) (hlevel 1)
from-total-predicate P .def (hx , _) = hx

from-total-predicate-is-equiv : is-equiv (from-total-predicate {A = A})
from-total-predicate-is-equiv = is-iso→is-equiv record where
  from P a = P .mem (always a)
  rinv P = ext λ a  Ω-ua
    (rec! λ ha  subst (_∈ P) (sym (is-always a ha)))
     pa  P .def pa , subst (_∈ P) (is-always a _) pa)
  linv P = ext λ a  Ω-ua snd (tt ,_)