---
layout: default
title : "Overture.Basic module"
date : "2021-01-13"
author: "the agda-algebras development team"
---
### 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
```agda
{-# 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](https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29)
and with it uniqueness of identity proofs; see the
[section on axiom K](https://agda.readthedocs.io/en/v2.8.0/language/without-k.html)
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](https://agda.readthedocs.io/en/v2.8.0/language/cubical-compatible.html)
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.
```agda
module Overture.Basic where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Product using ( ∃ ; Σ-syntax ; _×_ )
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ℓ
data 𝟚 : Type 0ℓ where 𝟎 : 𝟚 ; 𝟏 : 𝟚
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.
```agda
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.
```agda
_⁻¹ : {A : Type a} {x y : A} → x ≡ y → y ≡ x
p ⁻¹ = sym p
infix 40 _⁻¹
```
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.
```agda
_∙_ : {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 30 _∙_
```
#### Sigma types
The standard library's `∃[ x ] B`{.AgdaFunction} leaves the domain of
`x`{.AgdaBound} to inference, which reads as vague where a mathematician would
write `∃ x ∈ A, B`. `∃-syntax`{.AgdaFunction} is the alternative that displays
it — `∃[ x ∈ A ] B`{.AgdaFunction}, with `A`{.AgdaBound} the *type* of
`x`{.AgdaBound} — so the domain is stated rather than left to the reader. It
denotes the same type as `Σ[ x ∈ A ] B`{.AgdaFunction}, read "there exists an
`x` in `A` such that `B`" rather than "the type of pairs"; write whichever says
what is meant.
`A`{.AgdaBound} 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 `∃`{.AgdaFunction} would therefore turn `A` into a
token every use site had to spell verbatim, whatever its domain was called.
```agda
infix 2 ∃-syntax
∃-syntax : (A : Type a) → (A → Type b) → Type (a ⊔ b)
∃-syntax A = ∃ {A = A}
syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B
private
_ : {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.
```agda
Π : {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 6 Π-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](/Legacy/Base/Algebras/Basic/#lifts-of-algebras) 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.
```agda
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.)
```agda
module _ {A : Type a} {B : A → Type b } where
_≈_ : Π B → Π B → Type (a ⊔ b)
f ≈ g = ∀ x → f x ≡ g x
infix 8 _≈_
≈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.
```agda
≡-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.
```agda
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]
```agda
_⇔_ : {a b : Level} → Type a → Type b → Type (a ⊔ b)
P ⇔ Q = (P → Q) × (Q → P)
infix 1 _⇔_
```
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.)