------------------------------------------------------------------------ -- Experiments related to equality -- -- Nils Anders Danielsson -- -- Some files have been developed in collaboration with others, see -- the individual files. ------------------------------------------------------------------------ {-# OPTIONS --without-K #-} module README where -- Definitions of some basic types and some related functions. import Prelude -- Logical equivalences. import Logical-equivalence -- Two logically equivalent axiomatisations of equality. Many of the -- modules below are parametrised by a definition of equality that -- satisfies these axioms. The reason for this parametrisation is that -- I might later want to use a definition of equality where the -- application elim P r (refl x) does not compute to r x, unlike the -- equality in Equality.Propositional. (Equality.Tactic also contains -- a definition of equality which, roughly speaking, computes in this -- way.) import Equality -- One model of the axioms: propositional equality. import Equality.Propositional -- A simple tactic for proving equality of equality proofs (at the -- time of writing only used in Equality.Groupoid). import Equality.Tactic -- Injections. import Injection -- Split surjections. import Surjection -- Some definitions related to and properties of natural numbers. import Nat -- H-levels, along with some general properties. import H-level -- A proof which shows that sets with decidable equality have unique -- identity proofs. import Equality.Decidable-UIP -- Some decision procedures for equality. import Equality.Decision-procedures -- Bijections. import Bijection -- Groupoids. import Groupoid -- Equalities can be turned into groupoids which are sometimes -- commutative. import Equality.Groupoid -- Closure properties for h-levels. import H-level.Closure -- Preimages. import Preimage -- Equivalences. import Equivalence -- Embeddings. import Embedding -- A universe which includes several kinds of functions (ordinary -- functions, logical equivalences, injections, embeddings, -- surjections, bijections and equivalences). import Function-universe -- Results relating different instances of certain axioms related to -- equality. import Equality.Instances-related -- A parametrised specification of "natrec", along with a proof that -- the specification is propositional (assuming extensionality). import Nat.Eliminator -- Some definitions related to and properties of booleans. import Bool -- Monads. import Monad -- The double-negation monad. import Double-negation -- The univalence axiom. import Univalence-axiom -- The "interval". import Interval -- Truncation. import H-level.Truncation -- Propositional truncation. import H-level.Truncation.Propositional -- The "circle". import Circle -- Lists. import List -- Some definitions related to and properties of finite sets. import Fin -- M-types. import M -- Some definitions related to and properties of the Maybe type. import Maybe -- Vectors. import Vec -- Some properties related to the const function. import Const -- Some tactics aimed at making equational reasoning proofs more -- readable. import Tactic.By -- Quotients. import Quotient -- Quotients, defined using a higher inductive type. import Quotient.HIT -- Isomorphism of monoids on sets coincides with equality (assuming -- univalence). import Univalence-axiom.Isomorphism-is-equality.Monoid -- In fact, several large classes of algebraic structures satisfy the -- property that isomorphism coincides with equality (assuming -- univalence). import Univalence-axiom.Isomorphism-is-equality.Simple import Univalence-axiom.Isomorphism-is-equality.Simple.Variant import Univalence-axiom.Isomorphism-is-equality.More import Univalence-axiom.Isomorphism-is-equality.More.Examples -- A class of structures that satisfies the property that isomorphic -- instances of a structure are equal (assuming univalence). This code -- is superseded by the code above, but preserved because it is -- mentioned in a blog post. import Univalence-axiom.Isomorphism-implies-equality -- 1-categories. import Category import Functor import Adjunction -- Aczel's structure identity principle (for 1-categories). import Structure-identity-principle -- The structure identity principle can be used to establish that -- isomorphism coincides with equality (assuming univalence). import Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle -- Bag equivalence for lists. import Bag-equivalence -- Binary trees. import Tree -- Implementations of tree sort. One only establishes that the -- algorithm permutes its input, the other one also establishes -- sortedness. import Tree-sort.Partial import Tree-sort.Full import Tree-sort.Examples -- Containers, including a definition of bag equivalence. import Container -- An implementation of tree sort which uses containers to represent -- trees and lists. -- -- In the module Tree-sort.Full indexed types are used to enforce -- sortedness, but Containers contains a definition of non-indexed -- containers, so sortedness is not enforced in this development. -- -- The implementation using containers has the advantage of uniform -- definitions of Any/membership/bag equivalence, but the other -- implementations use more direct definitions and are perhaps a bit -- "leaner". import Container.List import Container.Tree import Container.Tree-sort import Container.Tree-sort.Example -- The stream container. import Container.Stream -- Record types with manifest fields and "with". import Record -- Overview of code related to some papers. import README.Bag-equivalence import README.Isomorphism-is-equality import README.Weak-J