Overture.Basic

Preliminaries

This is the Overture.Basic module of the Agda Universal Algebra Library.

Logical foundations

(See also the Equality module of the agda-algebras library.)

An Agda program typically begins by setting some options and by importing types from existing Agda libraries. Options are specified with the OPTIONS pragma and control the way Agda behaves by, for example, specifying the logical axioms and deduction rules we wish to assume when the program is type-checked to verify its correctness.

Each module in the library begins with a pragma line of the form

{-# OPTIONS --without-K --exact-split --safe #-}

• The --without-K flag disables the reasoning principles that are incompatible with univalent type theory, most importantly Streicher's axiom K and with it uniqueness of identity proofs; see the section on axiom K in the Agda manual. No proof in the library can appeal to K, so the library is compatible with type theories in which K fails, such as homotopy type theory.

For a time the library used the stronger flag --cubical-compatible, which implies --without-K and in addition makes Agda generate the internal support code that a module checked under --cubical needs in order to import this one. We returned to --without-K for three reasons.

• Version 3.0 of the Agda standard library is checked under --without-K, and a --cubical-compatible module cannot import a module that is not --cubical-compatible too. (Both flags are coinfective: a module checked under one may import only modules checked under it. A --without-K module may import a --cubical-compatible one, since the latter flag implies the former.) Keeping --cubical-compatible would have held the library to the 2.x standard library.
• Nothing imports the library from a --cubical module. The Cubical development planned for version 4.0 is to derive its modules from this library's by substitution, not to import them.
• The support code costs time and space. Checked from source, the library takes about 11% less time under --without-K than under --cubical-compatible, and its interface files take about 10% less space.

The price is that a --cubical module cannot import this library, just as it cannot import version 3.0 of the standard library. A future Cubical tree may import modules checked under --cubical or --cubical-compatible, such as those of the cubical library, but not this library's. ADR-011 records the decision and its measurements.

• The --exact-split flag requires every case in a definition by pattern matching to hold definitionally, not merely propositionally. This keeps the operational behavior of our definitions in lockstep with their intended mathematical meaning and catches accidental reliance on with-abstractions.

• Finally, --safe forbids postulates, trustMe, and unsafe FFI — everything in agda-algebras is a genuine proof.

Agda modules

The OPTIONS pragma is usually followed by the start of a module. For example, the Overture.Basic module begins with the following line, and then a list of imports of things used in the module.

module Overture.Basic where

open import Agda.Primitive using () renaming ( Set to  Type )

-- Imports from the Agda Standard Library -----------------------------------------------
open import Data.Product      using ( ∃ ; Σ-syntax ; _×_ )
-- `proj₁` / `proj₂` are re-exported, so the umbrella `Overture` supplies the
-- canonical projections that replace the deprecated `∣_∣` / `∥_∥` (ADR-002 §1).
open import Data.Product      using ( proj₁ ; proj₂ ) public
open import Function.Base     using ( _∘_ ; id )
open import Level             using ( Level ; suc ; _⊔_ ; lift ; lower ; Lift ; 0ℓ )
open import Relation.Binary   using ( IsEquivalence )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans )

private variable a b : Level

ℓ₁ : Level
ℓ₁ = suc 0ℓ

-- the two element type
data 𝟚 : Type 0ℓ where 𝟎 : 𝟚 ;  𝟏 : 𝟚

-- the three element type
data 𝟛 : Type 0ℓ where 𝟎 : 𝟛 ;  𝟏 : 𝟛 ;  𝟐 : 𝟛

Projection notation

The definition of Σ (and thus, of ×) includes the fields proj₁ and proj₂ representing the first and second projections out of the product. Sometimes we prefer to denote these projections by ∣_∣ and ∥_∥, respectively. We define these alternative notations for projections out of pairs as follows.

module _ {A : Type a}{B : A → Type b} where

  ∣_∣ : Σ[ x ∈ A ] B x → A
  ∣_∣ = proj₁

  ∥_∥ : (z : Σ[ a ∈ A ] B a) → B (proj₁ z)
  ∥_∥ = proj₂

  {-# WARNING_ON_USAGE ∣_∣
  "The bracket projection `∣_∣` is deprecated (v3.0); it is being replaced
   library-wide by `proj₁` (from `Data.Product`), with `OperationSymbolsOf` for
   signature components.  See ADR-002 §1.  Retained so `Legacy/` keeps compiling."
  #-}
  {-# WARNING_ON_USAGE ∥_∥
  "The bracket projection `∥_∥` is deprecated (v3.0); it is being replaced
   library-wide by `proj₂` (from `Data.Product`), with `ArityOf` for signature
   components.  See ADR-002 §1.  Retained so `Legacy/` keeps compiling."
  #-}

Here we put the definitions inside an anonymous module, which starts with the module keyword followed by an underscore (instead of a module name). The purpose is simply to move the postulated typing judgments---the "parameters" of the module (e.g., A : Type a)---out of the way so they don't obfuscate the definitions inside the module.

Let's define some useful syntactic sugar that will make it easier to apply symmetry and transitivity of ≡ in proofs.

_⁻¹ : {A : Type a} {x y : A} → x ≡ y → y ≡ x
p ⁻¹ = sym p

infix   _⁻¹

If we have a proof p : x ≡ y, and we need a proof of y ≡ x, then instead of sym p we can use the more intuitive p ⁻¹. Similarly, the following syntactic sugar makes abundant appeals to transitivity easier to stomach.

_∙_ : {A : Type a}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
p ∙ q = trans p q

𝑖𝑑 : (A : Type a) → A → A
𝑖𝑑 A = λ x → x

infixl  _∙_

Sigma types

The standard library's ∃[ x ] B leaves the domain of x to inference, which reads as vague where a mathematician would write ∃ x ∈ A, B. ∃-syntax is the alternative that displays it — ∃[ x ∈ A ] B, with A the type of x — so the domain is stated rather than left to the reader. It denotes the same type as Σ[ x ∈ A ] B, read "there exists an x in A such that B" rather than "the type of pairs"; write whichever says what is meant.

A is an explicit argument, which is what makes the notation honest: a syntax declaration's right-hand side may only mention names bound on its left, and anything else in it is a literal token. Declaring this notation over the implicit-domain ∃ would therefore turn A into a token every use site had to spell verbatim, whatever its domain was called.

infix  ∃-syntax

∃-syntax : (A : Type a) → (A → Type b) → Type (a ⊔ b)
∃-syntax A = ∃ {A = A}

syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B

private
  -- Canary: the domain is bound by the notation, so *any* type may stand to the
  -- right of `∈` — the point of the declaration.  (Under a declaration that left
  -- the domain implicit, `A` would be a literal token and this would not parse.)
  _ : {X : Type a} {P : X → Type b} → (∃[ x ∈ X ] P x) → Σ[ x ∈ X ] P x
  _ = λ z → z

Pi types

The dependent function type is traditionally denoted with an uppercase pi symbol and typically expressed as Π(x : A) B x, or something similar. In Agda syntax, one writes (x : A) → B x for this dependent function type, but we can define syntax that is closer to standard notation as follows.

Π : {A : Type a } (B : A → Type b ) → Type (a ⊔ b)
Π {A = A} B = (x : A) → B x

Π-syntax : (A : Type a)(B : A → Type b) → Type (a ⊔ b)
Π-syntax A B = Π B

syntax Π-syntax A (λ x → B) = Π[ x ∈ A ] B
infix  Π-syntax

In the modules that follow, we will see many examples of this syntax in action.

Agda's universe hierarchy

The hierarchy of universes in Agda is structured as follows:

Type a : Type (lsuc a), Type (lsuc a) : Type (lsuc (lsuc a)) , etc.

and so on. This means that the universe Type a has type Type(lsuc a), and Type(lsuc a) has type Type(lsuc (lsuc a)), and so on. It is important to note, however, this does not imply that Type a : Type(lsuc(lsuc a)). In other words, Agda's universe hierarchy is non-cumulative. This makes it possible to treat universe levels more precisely, which is nice. On the other hand, a non-cumulative hierarchy can sometimes make for a non-fun proof assistant. Specifically, in certain situations, the non-cumulativity makes it unduly difficult to convince Agda that a program or proof is correct.

Lifting and lowering

Here we describe a general Lift type that help us overcome the technical issue described in the previous subsection. In the Lifts of algebras section of the Legacy.Base.Algebras.Basic module we will define a couple domain-specific lifting types which have certain properties that make them useful for resolving universe level problems when working with algebra types.

Let us be more concrete about what is at issue here by considering a typical example. Agda will often complain with errors like the following:

Birkhoff.lagda:498,20-23
a != 𝓞 ⊔ 𝓥 ⊔ (lsuc a) when checking that the expression... has type...

This error message means that Agda encountered the universe level lsuc a, on line 498 (columns 20--23) of the file Birkhoff.lagda, but was expecting a type at level 𝓞 ⊔ 𝓥 ⊔ lsuc a instead.

The general Lift record type that we now describe makes such problems easier to deal with. It takes a type inhabiting some universe and embeds it into a higher universe and, apart from syntax and notation, it is equivalent to the Lift type one finds in the Level module of the Agda Standard Library.

record Lift {𝓦 a : Level} (A : Set a) : Set (a ⊔ 𝓦) where
  constructor lift
  field
    lower : A

The point of having a ramified hierarchy of universes is to avoid Russell's paradox, and this would be subverted if we were to lower the universe of a type that wasn't previously lifted. However, we can prove that if an application of lower is immediately followed by an application of lift, then the result is the identity transformation. Similarly, lift followed by lower is the identity.

lift∼lower : {A : Type a} → lift ∘ lower ≡ 𝑖𝑑 (Lift b A)
lift∼lower = refl

lower∼lift : {A : Type a} → (lower {a}{b}) ∘ lift ≡ 𝑖𝑑 A
lower∼lift = refl

The proofs are trivial. Nonetheless, we'll come across some holes these lemmas can fill.

Pointwise equality of dependent functions

We conclude this module with a definition that conveniently represents te assertion that two functions are (extensionally) the same in the sense that they produce the same output when given the same input. (We will have more to say about this notion of equality in the Legacy.Base.Equality.Extensionality module.)

module _ {A : Type a} {B : A → Type b } where

  _≈_ : Π B → Π B → Type (a ⊔ b)
  f ≈ g = ∀ x → f x ≡ g x

  infix  _≈_

  ≈IsEquivalence : IsEquivalence _≈_
  IsEquivalence.refl   ≈IsEquivalence          = λ _ → refl
  IsEquivalence.sym    ≈IsEquivalence f≈g      = sym ∘ f≈g
  IsEquivalence.trans  ≈IsEquivalence f≈g g≈h  = λ x → trans (f≈g x) (g≈h x)

The following is convenient for proving two pairs of a product type are equal using the fact that their respective components are equal.

≡-by-parts : {A : Type a} {B : Type b} {u v : A × B}
  → proj₁ u ≡ proj₁ v → proj₂ u ≡ proj₂ v → u ≡ v

≡-by-parts refl refl = refl

Lastly, we will use the following type (instead of subst) to transport equality proofs.

transport : {A : Type a } (B : A → Type b) {x y : A} → x ≡ y → B x → B y
transport B refl = id

Logical equivalence helper

For simple logical equivalence of types, we define a small helper that packages the two implications into a single two-way implication.[^2]

_⇔_ : {a b : Level} → Type a → Type b → Type (a ⊔ b)
P ⇔ Q = (P → Q) × (Q → P)
infix  _⇔_

The standard library's _⇔_ is the bundled Function.Bundles.Equivalence record, carrying congruence proofs; here the lighter logical equivalence — a pair of functions — is all that simple Type-level statements require.)