↑ Top


Preliminaries

This is the Base.Overture.Preliminaries module of the agda-algebras 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. Every Agda program in agda-algebras begins with the following line.

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

These options control certain foundational assumptions that Agda makes when type-checking the program to verify its correctness.

Note that if we wish to type-check a file that imports another file that still has some unmet proof obligations, we must replace the --safe flag with --allow-unsolved-metas, but this is never done in (publicly released versions of) the agda-algebras library.

Agda Modules

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

module Base.Overture.Preliminaries where

-- Imports from Agda and the Agda Standard Library -----------------------------------------------
open import Agda.Primitive   using ( _⊔_ ; lsuc ) renaming ( Set to  Type ; lzero to  ℓ₀ )
open import Data.Product     using ( _,_ ;  ; Σ-syntax ; _×_ ) renaming ( proj₁ to fst ; proj₂ to snd )
open import Function.Base    using ( _∘_ ; id )
open import Level            using ( Level ; Lift ; lift ; lower )
open import Relation.Binary  using ( Decidable )
open import Relation.Binary.Structures using ( IsEquivalence ; IsPartialOrder )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans )
open import Relation.Nullary using ( Dec ; yes ; no ; Irrelevant )
private variable α β : Level

ℓ₁ : Level
ℓ₁ = lsuc ℓ₀

-- the two element type
data 𝟚 : Type ℓ₀ where  -- We could use Bool instead.
 𝟎 : 𝟚 ;  𝟏 : 𝟚

-- the three element type
data 𝟛 : Type ℓ₀ 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. However, we prefer the shorter names fst and snd. 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 α }{B : A  Type β} where

 ∣_∣ : Σ[ x  A ] B x  A
 ∣_∣ = fst

 ∥_∥ : (z : Σ[ a  A ] B a)  B  z 
 ∥_∥ = snd

 infix  40 ∣_∣

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 α)—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 α} {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.

_∙_ : {A : Type α}{x y z : A}  x  y  y  z  x  z
p  q = trans p q

𝑖𝑑 : (A : Type α )  A  A
𝑖𝑑 A = λ x  x

infixl 30 _∙_

Sigma types

infix 2 ∃-syntax

∃-syntax :  {A : Type α}  (A  Type β)  Set (α  β)
∃-syntax = 

syntax ∃-syntax  x  B) = ∃[ x  A ] B

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 α } (B : A  Type β )  Type (α  β)
Π {A = A} B = (x : A)  B x

Π-syntax : (A : Type α)(B : A  Type β)  Type (α  β)
Π-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 α : Type (lsuc α) ,   Type (lsuc α) : Type (lsuc (lsuc α)) , etc.

and so on. This means that the universe Type α has type Type(lsuc α), and Type(lsuc α) has type Type(lsuc (lsuc α)), and so on. It is important to note, however, this does not imply that Type α : Type(lsuc(lsuc α)). 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 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
α != 𝓞 ⊔ 𝓥 ⊔ (lsuc α) when checking that the expression... has type...

This error message means that Agda encountered the universe level lsuc α, on line 498 (columns 20–23) of the file Birkhoff.lagda, but was expecting a type at level 𝓞 ⊔ 𝓥 ⊔ lsuc α 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 {𝓦 α : Level} (A : Set α) : Set (α ⊔ 𝓦) 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 α}  lift  lower  𝑖𝑑 (Lift β A)
lift∼lower = refl

lower∼lift : {A : Type α}  (lower {α}{β})  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 Base.Equality.Extensionality module.)

module _ {α : Level}{A : Type α}{β : Level}{B : A  Type β } where

 _≈_ :  (f g : (a : A)  B a)  Type (α  β)
 f  g =  x  f x  g x

 infix 8 _≈_

 ≈IsEquivalence : IsEquivalence _≈_
 IsEquivalence.refl ≈IsEquivalence = λ _  refl
 IsEquivalence.sym ≈IsEquivalence {f}{g} f≈g = λ x  sym (f≈g x)
 IsEquivalence.trans ≈IsEquivalence {f}{g}{h} 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 α}{B : Type β}{u v : A × B}  fst u  fst v  snd u  snd 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 α } (B : A  Type β) {x y : A}  x  y  B x  B y
transport B refl = id


↑ Base.Overture Base.Overture.Inverses →