------------------------------------------------------------------------
-- Experiments related to equality
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module README where

-- Definitions of some basic types and some related functions.

import Prelude

-- Equivalences.

import Equivalence

-- Two equivalent axiomatisations of equality. Most of the modules
-- below are parametrised by a definition of equality which 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

-- Some decision procedures for equality.

import Equality.Decision-procedures

-- A proof which shows that sets with decidable equality have unique
-- identity proofs.

import Equality.Decidable-UIP

-- Groupoids.

import Groupoid

-- Equalities can be turned into groupoids which are sometimes
-- commutative.

import Equality.Groupoid

-- Injections.

import Injection

-- Surjections.

import Surjection

-- Bijections.

import Bijection

-- All instances of the equality axioms are isomorphic.

import Equality.Instances-isomorphic

-- H-levels, along with some general properties.

import H-level

-- Closure properties for h-levels.

import H-level.Closure

-- Preimages.

import Preimage

-- Weak equivalences.

import Weak-equivalence

-- The univalence axiom.

import Univalence-axiom

-- A universe which includes several kinds of functions (ordinary
-- functions, equivalences, injections, surjections, bijections and
-- weak equivalences).

import Function-universe

-- Some definitions related to and properties of finite sets.

import Fin

-- Bag equivalence for lists.

import Bag-equivalence

-- 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