Graphs of recursive definitions

A recursion in L gives a unique value at every point of an internal domain. A set-theoretic function is represented by its graph, the set of ordered pairs pr(x , y) with input first and output second. This chapter turns the value relation of a recursion into such a set F, then proves that F is functional and has exactly the original domain.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Recursion.Graph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )

The graph must itself be described in the object language. The available syntax forms conjunctions and existential statements, while renaming places an existing two-variable value relation beneath a new quantifier. The ambient operation pr supplies ordered-pair codes, and its injectivity later recovers both coordinates from an equality of codes.

open import FOL.Syntax using ( Formula; _∧̇_; ∃̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj )

The constructible pairing operation produces an element of L whose underlying set is the ambient ordered-pair code. The general recursion theorem can then apply replacement to a formula describing those pairs. Equality of constructible elements is reduced to equality of their underlying sets because constructibility proofs are propositions.

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion; module Of )
open import L.Coding.Model {ℓ}
  using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; domAt; domAt-intro )

open import Cubical.Data.Sigma using ( Σ≡Prop )

Several propositions below are obtained from truncated existence statements. They may be eliminated only into propositional goals. Membership and equality in the cumulative hierarchy have precisely this property, which allows witnesses to be used without making a global choice.

open import Cubical.Foundations.HLevels using ( isPropΣ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )

The formulas are interpreted in the constructible structure. The local satisfaction notation and its renaming theorem connect syntactic substitutions with changes of environment; all later claims about the graph are statements in this semantics.

open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
module PairFo (φ : Formula S ) where

A formula for ordered pairs

Fix a two-variable formula φ, read as a relation between a value and an index. The module PairFo constructs another two-variable formula: at a candidate pair e and an index p, it asserts that some value z satisfies φ(z,p) and that e is the ordered pair pr(p,z).

  ρ : Fin  → Fin 
  ρ zero       = zero
  ρ (suc zero) = suc (suc zero)

The renaming map records how the two free variables of φ occur below the existential quantifier. The value variable remains in slot zero and is bound by that quantifier; the index variable moves to slot two. The formula pairFo is opaque, so subsequent reasoning uses its proved semantic characterization rather than unfolding it.

  opaque
    pairFo : Formula S 

The formula conjoins two assertions under the existential quantifier. The first says that e codes the ordered pair of p and the quantified value; the second is the renamed copy of φ. Thus the syntax directly mirrors the mathematical description of a member of a function graph.

    pairFo = ∃̇ (prAtL (suc zero) (suc (suc zero)) zero ∧̇ renameFo ρ φ)

The agreement proof verifies that renaming preserves the intended environment. In the longer environment (z ∷ e ∷ p ∷ []), the renamed value slot reads z and the renamed index slot reads p, exactly as the original formula does in (z ∷ p ∷ []).

    private
      ag : (z e p : S) → Ren.Agrees ρ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ [])
      ag z e p zero       = refl
      ag z e p (suc zero) = refl

Two semantic equalities prepare the outward direction. Correctness of the ordered-pair formula identifies its satisfaction with the ambient equality fst e ≡ pr (fst p) (fst z). The renaming theorem identifies satisfaction of the renamed formula with satisfaction of the original φ at value z and index p.

      at : (z e p : S)
         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
         ≡ (fst e ≡ pr (fst p) (fst z))
      at z e p = cong ⟨_⟩ (prAtL-adequate (suc zero) (suc (suc zero)) zero (z ∷ e ∷ p ∷ []))

      gr : (z e p : S)

Reading pairFo outward yields a propositionally truncated value z, together with the ordered-pair equation and a proof of φ(z,p). Reading it inward reverses these transports: such a value, equation, and graph proof construct a satisfaction witness for pairFo. These are the two semantic directions used below.

         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ renameFo ρ φ ⟩ ≡ ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
      gr z e p = cong ⟨_⟩ (Ren.⊨-rename ρ φ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) (ag z e p))

    pair-out : (e p : S) → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
             → ∥ Σ[ z ∈ S ] ((fst e ≡ pr (fst p) (fst z)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
    pair-out e p = PT.map (λ { (z , (q , h)) →

The inward lemma completes the semantic equivalence and the construction now turns to a fixed recursion. Its original domain and value relation are retained; only the values sent to replacement will change from bare outputs to ordered pairs of inputs and outputs.

      z , (transport (at z e p) q , transport (gr z e p) h) })

    pair-in : (e p z : S) → fst e ≡ pr (fst p) (fst z) → ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
            → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
    pair-in e p z q h = ∣ z , (transport (sym (at z e p)) q , transport (sym (gr z e p)) h) ∣₁
module Graph (R₀ : Recursion) where

Domain and values

The recursion supplies a domain, its original graph formula, and contractibility of the graph-value fiber at each domain member. Its derived value is written fn. The local predicate Mem x is the underlying membership assertion that fn requires.

  open Of R₀ public using ( dom; graph; funct ) renaming ( val to fn )
  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst dom ⟩

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst dom)

Membership in a set is proposition-valued, so Mem x is a proposition. Consequently, any two proofs that x belongs to the domain are equal. This proof irrelevance ensures that the value fn x m does not depend on the chosen membership certificate.

  private
    defines : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    defines x m = funct x m .fst .snd

    only : (x : S) (m : Mem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
    only x m y h = sym (cong fst (funct x m .snd (y , h)))

Contractibility provides two facts about the original value relation. The selected centre proves that the formula graph is satisfied in the environment (fn x m ∷ x ∷ []). Its contraction proves that any other y satisfying the formula at x equals fn x m.

    module Fo = PairFo graph renaming ( pairFo to fo; pair-out to out; pair-in to into )

    fn-irr : (x : S) (m m' : Mem x) → fn x m ≡ fn x m'
    fn-irr x m m' = cong (fn x) (isPropMem x m m')
    pairOf : (x : S) → Mem x → S
    pairOf x m = prʟ x (fn x m)

The ordered-pair formula is now specialized to the original value relation. Proof irrelevance for Mem x gives fn-irr, while pairOf x m is the constructible ordered pair of x and its value. Its underlying set is pr (fst x) (fst (fn x m)).

    uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
    uniq x m p h = PT.rec (isSetS p (pairOf x m))
      (λ { (z , (e , g)) → Σ≡Prop (λ v → snd (isL v))
        (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z g) ∙ sym (prʟ-fst x (fn x m))) })
      (Fo.out p x h)

Suppose a candidate p satisfies the specialized pair formula at x. The outward lemma merely supplies a value z, an equality between the underlying set of p and pr(x,z), and a proof that z satisfies the original graph. Original-value uniqueness identifies z with fn x m; composing the resulting equalities proves p ≡ pairOf x m.

    R : Recursion
    R = record
      { dom   = dom
      ; graph = Fo.fo
      ; funct = λ x m →

Collecting the graph

A new recursion uses the same domain and the ordered-pair formula as its value relation. At x, its centre is pairOf x m; the inward semantic lemma proves that this pair satisfies the formula, and uniq proves that every other satisfying candidate is equal to it.

          ( pairOf x m
          , Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m) )
        , λ { (p , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ Fo.fo)) (sym (uniq x m p h)) } }

    module T = Of R using ( table; table-in; table-out )

  F : S

The dependent-pair contraction compares a candidate value together with its satisfaction proof against the chosen centre. Equality of their first components is uniq; the satisfaction components are propositions, so this equality determines the whole dependent-pair path. The result is a valid Recursion for ordered pairs.

  F = T.table

  F-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst F ⟩
  F-in x m = subst (λ w → ⟨ w ∈ fst F ⟩) (prʟ-fst x (fn x m))
    (T.table-in x (pairOf x m) m
      (Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m)))

Replacement applied to this recursion forms the value range of its ordered-pair values. That range is the desired graph F. Thus F is an element of L, and every element placed in it is an ordered pair of a domain element with its recursively determined value.

  F-out : (p : V ℓ) → ⟨ p ∈ fst F ⟩
        → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
  F-out p h = PT.rec squash₁ step (T.table-out pS h)
    where
    pS : S

The inward membership direction is immediate from the replacement specification. For a domain witness m, the constructible ordered pair pairOf x m satisfies the pair formula, hence belongs to the replacement range. Transport along prʟ-fst restates this as membership of the ambient code pr (fst x) (fst (fn x m)) in the underlying set of F.

    pS = p , isL-trans {x = fst F} {y = p} h (snd F)

    step : Σ[ x ∈ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩)
         → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
    step (x , (m , g)) = PT.map
      (λ { (z , (e , gz)) →

For the outward direction, begin with an ambient set p ∈ fst F. Downward closure of constructibility packages p as an element pS of L. The replacement specification first yields, merely, an index x, a domain proof m, and satisfaction of the ordered-pair formula by pS.

        x , m , (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z gz)) })
      (Fo.out pS x g)
  Fib : S → S → Type (ℓ-suc ℓ)
  Fib x y = Σ[ m ∈ Mem x ] (fst y ≡ fst (fn x m))

  isPropFib : (x y : S) → isProp (Fib x y)

The semantic outward lemma then opens a second truncation and supplies a value z, an ordered-pair equality, and a proof of the original graph relation. Original-value uniqueness replaces z by fn x m. The result states merely that p is the code pr(x,fn x m) for some domain element x.

  isPropFib x y = isPropΣ (isPropMem x) (λ m → setIsSet (fst y) (fst (fn x m)))

  pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → Fib x y
  pair-out x y h = PT.rec (isPropFib x y) step (F-out (pr (fst x) (fst y)) h)
    where
    step : Σ[ x' ∈ S ] Σ[ m' ∈ Mem x' ] (pr (fst x) (fst y) ≡ pr (fst x') (fst (fn x' m')))

Recovering the coordinates

For fixed x and y, the fiber Fib x y consists of a domain proof m : Mem x and an equality between the underlying set of y and that of fn x m. Both components are propositions: domain membership is proposition-valued and equality in V is a proposition. Hence the whole fiber is a proposition.

         → Fib x y
    step (x' , m' , e) = subst (λ z → Fib z y)
      (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)

  γ : S ^ 
  γ = F ∷ dom ∷ []

If the ordered-pair code pr(fst x,fst y) belongs to F, the outward description gives x', m', and an equality with pr(fst x',fst(fn x' m')). Injectivity of pr yields equalities of both coordinates. The input equality transports m' to a proof that x lies in the domain; the output equality gives the second component of Fib x y.

  sv : ⟨ γ ⊨ svAt zero ⟩
  sv = svAt-in zero γ (λ x y y' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x y' q
    in e ∙ cong fst (fn-irr x m m') ∙ sym e')

The environment γ = F ∷ dom ∷ [] assigns the two free variables used by the formulas for single-valuedness and domain. To prove single-valuedness, take two pairs in F with the same first coordinate x. Their fibers provide membership proofs m and m' and output equalities to fn x m and fn x m'. Proof irrelevance identifies the two function values, so the outputs are equal.

  dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
  dm = domAt-intro zero (suc zero) γ (λ x → fwd x , bwd x)
    where
    fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩ → Mem x
    fwd x = PT.rec (isPropMem x) (λ { (y , p) → fst (pair-out x y p) })

Finally, the domain formula is proved in both directions. If x occurs as the first coordinate of some ordered pair in F, pair-out returns a fiber and hence a proof Mem x. Conversely, from m : Mem x, the pair pr(x,fn x m) belongs to F by F-in, so x occurs as a first coordinate. Therefore the domain of the collected graph is exactly dom.

    bwd : (x : S) → Mem x → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩
    bwd x m = ∣ fn x m , F-in x m ∣₁