------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about how mathematical hierarchies are laid out.
------------------------------------------------------------------------
{-# OPTIONS --allow-unsolved-metas #-}
module README.Design.Hierarchies where
open import Data.Sum.Base using (_⊎_)
open import Level using (Level; _⊔_; suc)
open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_)
private
variable
a b ℓ : Level
A : Set a
------------------------------------------------------------------------
-- Introduction
------------------------------------------------------------------------
-- One of the key design decisions facing the library is how to handle
-- mathematical hierarchies, e.g.
-- ∙ Binary relations: preorder → partial order → total order
-- ↘ equivalence
-- ∙ Algebraic structures: magma → semigroup → monoid → group
-- ↘ band → semilattice
--
-- Some of the hierarchies in the library are:
-- ∙ Algebra
-- ∙ Function
-- ∙ Relation.Binary
-- ∙ Relation.Binary.Indexed
--
-- A given hierarchy `X` is always split into 4 seperate folders:
-- ∙ X.Core
-- ∙ X.Definitions
-- ∙ X.Structures
-- ∙ X.Bundles
-- all four of which are publicly re-exported by `X` itself.
--
-- Additionally a hierarchy `X` may contain additional files
-- ∙ X.Bundles.Raw
-- ∙ X.Consequences
-- ∙ X.Constructs
-- ∙ X.Properties
-- ∙ X.Morphisms
--
-- Descriptions of these modules are now described below using the
-- running example of the `Relation.Binary` and `Algebra` hierarchies.
-- Note that we redefine everything here for illustrative purposes,
-- and that the definitions given below may be slightly simpler
-- than the real definitions in order to focus on the points being
-- discussed.
------------------------------------------------------------------------
-- Main hierarchy modules
------------------------------------------------------------------------
------------------------------------------------------------------------
-- X.Core
-- The Core module contains the basic units of the hierarchy.
-- For example for binary relations these are homoegeneous and
-- heterogeneous binary relations:
REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ
Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = A → A → Set ℓ
-- and in Algebra these are unary and binary operators, e.g.
Op₁ : Set a → Set a
Op₁ A = A → A
Op₂ : Set a → Set a
Op₂ A = A → A → A
------------------------------------------------------------------------
-- X.Definitions
-- The Definitions module defines the various properties that the
-- basic units of the hierarchy may have.
-- For example in Relation.Binary this includes reflexivity,
-- transitivity etc.
Reflexive : Rel A ℓ → Set _
Reflexive _∼_ = ∀ {x} → x ∼ x
Symmetric : Rel A ℓ → Set _
Symmetric _∼_ = ∀ {x y} → x ∼ y → y ∼ x
Transitive : Rel A ℓ → Set _
Transitive _∼_ = ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z
Total : Rel A ℓ → Set _
Total _∼_ = ∀ x y → x ∼ y ⊎ y ∼ x
-- For example in Algebra these are associativity, commutativity.
-- Note that all definitions for Algebra are based on some notion of
-- underlying equality.
Associative : Rel A ℓ → Op₂ A → Set _
Associative _≈_ _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
Commutative : Rel A ℓ → Op₂ A → Set _
Commutative _≈_ _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
LeftIdentity : Rel A ℓ → A → Op₂ A → Set _
LeftIdentity _≈_ e _∙_ = ∀ x → (e ∙ x) ≈ x
RightIdentity : Rel A ℓ → A → Op₂ A → Set _
RightIdentity _≈_ e _∙_ = ∀ x → (x ∙ e) ≈ x
-- Note that the types in `Definitions` modules are not meant to express
-- the full concept on their own. For example the `Associative` type does
-- not require the underlying relation to be an equivalence relation.
-- Instead they are designed to aid the modular reuse of the core
-- concepts. The complete concepts are captured in various
-- structures/bundles where the definitions are correctly used in
-- context.
------------------------------------------------------------------------
-- X.Structures
-- When an abstract hierarchy of some sort (for instance semigroup →
-- monoid → group) is included in the library the basic approach is to
-- specify the properties of every concept in terms of a record
-- containing just properties, parameterised on the underlying
-- sets, relations and operations. For example:
record IsEquivalence {A : Set a}
(_≈_ : Rel A ℓ)
: Set (a ⊔ ℓ)
where
field
refl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_
-- More specific concepts are then specified in terms of the simpler
-- ones:
record IsMagma {A : Set a} (≈ : Rel A ℓ) (∙ : Op₂ A) : Set (a ⊔ ℓ) where
field
isEquivalence : IsEquivalence ≈
∙-cong : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
record IsSemigroup {A : Set a} (≈ : Rel A ℓ) (∙ : Op₂ A) : Set (a ⊔ ℓ) where
field
isMagma : IsMagma ≈ ∙
associative : Associative ≈ ∙
open IsMagma isMagma public
-- Note here that `open IsMagma isMagma public` ensures that the
-- fields of the `isMagma` record can be accessed directly; this
-- technique enables the user of an `IsSemigroup` record to use underlying
-- records without having to manually open an entire record hierarchy.
-- This is not always possible, though. Consider the following definition
-- of preorders:
record IsPreorder {A : Set a}
(_≈_ : Rel A ℓ) -- The underlying equality.
(_∼_ : Rel A ℓ) -- The relation.
: Set (a ⊔ ℓ) where
field
isEquivalence : IsEquivalence _≈_
refl : Reflexive _∼_
trans : Transitive _∼_
module Eq = IsEquivalence isEquivalence
-- The IsEquivalence field in IsPreorder is not opened publicly because
-- the `refl` and `trans` fields would clash with those in the
-- `IsPreorder` record. Instead we provide an internal module and the
-- equality fields can be accessed via `Eq.refl` and `Eq.trans`.
------------------------------------------------------------------------
-- X.Bundles
-- Although structures are useful for describing the properties of a
-- given set of operations/relations, sometimes you don't require the
-- properties to hold for a given set of objects but only that such a
-- set of objects exists. In this case bundles are what you're after.
-- Each structure has a corresponding bundle that include the structure
-- along with the corresponding sets, relations and operations as
-- fields.
record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
open IsEquivalence isEquivalence public
-- The contents of the structure is always re-exported publicly,
-- providing access to its fields.
record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isMagma : IsMagma _≈_ _∙_
open IsMagma isMagma public
record Semigroup : Set (suc (a ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set a
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
isSemigroup : IsSemigroup _≈_ _∙_
open IsSemigroup isSemigroup public
magma : Magma a ℓ
magma = record { isMagma = isMagma }
-- Note that the Semigroup record does not include a Magma field.
-- Instead the Semigroup record includes a "repackaging function"
-- semigroup which converts a Magma to a Semigroup.
-- The above setup may seem a bit complicated, but it has been arrived
-- at after a lot of thought and is designed to both make the hierarchies
-- easy to work with whilst also providing enough flexibility for the
-- different applications of their concepts.
-- NOTE: bundles for the function hierarchy are designed a little
-- differently, as a function with an unknown domain an codomain is
-- of little use.
-------------------------
-- Bundle re-exporting --
-------------------------
-- In general ensuring that bundles re-export everything in their
-- sub-bundles can get a little tricky.
-- Imagine we have the following general scenario where bundle A is a
-- direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field)
-- but is also morally a refinement of bundles B and D.
-- Structures Bundles
-- ========== =======
-- IsA A
-- / || \ / || \
-- IsB IsC IsD B C D
-- The procedure for re-exports in the bundles is as follows:
-- 1. `open IsA isA public using (IsC, M)` where `M` is everything
-- exported by `IsA` that is not exported by `IsC`.
-- 2. Construct `c : C` via the `isC` obtained in step 1.
-- 3. `open C c public hiding (N)` where `N` is the list of fields
-- shared by both `A` and `C`.
-- 4. Construct `b : B` via the `isB` obtained in step 1.
-- 5. `open B b public using (O)` where `O` is everything exported
-- by `B` but not exported by `IsA`.
-- 6. Construct `d : D` via the `isC` obtained in step 1.
-- 7. `open D d public using (P)` where `P` is everything exported
-- by `D` but not exported by `IsA`
------------------------------------------------------------------------
-- Other hierarchy modules
------------------------------------------------------------------------
------------------------------------------------------------------------
-- X.Bundles.Raw
-- Sometimes it is useful to have the bundles without any accompanying
-- laws. These correspond more or less to what the definitions would
-- be in non-dependently typed languages like Haskell.
-- Each bundle thereofre has a corresponding raw bundle that only
-- include the laws but not the operations.
record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
infixl 7 _∙_
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
_∙_ : Op₂ Carrier
ε : Carrier
------------------------------------------------------------------------
-- X.Consequences
-- The "consequences" modules contains proofs for how the different
-- types in the `Definitions` module relate to each other. For example:
-- that any total relation is reflexive or that commutativity allows
-- one to translate between left and right identities.
total⇒refl : ∀ {_∼_ : Rel A ℓ} → Total _∼_ → Reflexive _∼_
total⇒refl = {!!}
idˡ+comm⇒idʳ : ∀ {_≈_ : Rel A ℓ} {e _∙_} → Commutative _≈_ _∙_ →
LeftIdentity _≈_ e _∙_ → RightIdentity _≈_ e _∙_
idˡ+comm⇒idʳ = {!!}
------------------------------------------------------------------------
-- X.Construct
-- The "construct" folder contains various generic ways of constructing
-- new instances of the hierarchy. For example
import Relation.Binary.Construct.Intersection
-- takes in two relations and forms the new relation that says two
-- elements are only related if they are related via both of the
-- original relations.
-- These files are layed out in four parts, mimicking the main modules
-- of the hierarchy itself. First they define the new relation, then
-- subsequently how the definitions, then structures and finally
-- bundles can be translated across to it.
------------------------------------------------------------------------
-- X.Morphisms
-- The `Morphisms` folder is a sub-hierarchy containing relationships
-- such homomorphisms, monomorphisms and isomorphisms between the
-- structures and bundles in the hierarchy.
------------------------------------------------------------------------
-- X.Properties
-- The `Properties` folder contains additional proofs about the theory
-- of each bundle. They are usually designed so as a bundle's
-- `Properties` file re-exports the contents of the `Properties` files
-- above it in the hierarchy. For example
-- `Algebra.Properties.AbelianGroup` re-exports the contents of
-- `Algebra.Properties.Group`.