Index of /~nad/listings/equality

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.css 12-Jul-2018 14:21 1.2K 
[TXT]Agda.Builtin.Unit.html 12-Jul-2018 14:21 1.2K 
[TXT]Agda.Builtin.Word.html 12-Jul-2018 14:21 1.7K 
[TXT]README.Weak-J.html 12-Jul-2018 14:21 1.8K 
[TXT]Agda.Builtin.Equalit..>12-Jul-2018 14:21 2.3K 
[TXT]Agda.Builtin.Bool.html 12-Jul-2018 14:21 2.4K 
[TXT]Agda.Builtin.Size.html 12-Jul-2018 14:21 2.9K 
[TXT]Agda.Builtin.Int.html 12-Jul-2018 14:21 3.1K 
[TXT]Agda.Builtin.List.html 12-Jul-2018 14:21 3.6K 
[TXT]Agda.Primitive.html 12-Jul-2018 14:21 3.6K 
[TXT]Agda.Builtin.Char.html 12-Jul-2018 14:21 3.7K 
[TXT]Agda.Builtin.String...>12-Jul-2018 14:21 5.1K 
[TXT]Container.Tree-sort...>12-Jul-2018 14:21 7.5K 
[TXT]README.Isomorphism-i..>12-Jul-2018 14:21 10K 
[TXT]Agda.Builtin.Float.html12-Jul-2018 14:21 10K 
[TXT]README.Bag-equivalen..>12-Jul-2018 14:21 11K 
[TXT]Tree-sort.Examples.html12-Jul-2018 14:21 11K 
[TXT]Equality.Proposition..>12-Jul-2018 14:21 13K 
[TXT]README.html 12-Jul-2018 14:21 16K 
[TXT]Injection.html 12-Jul-2018 14:21 17K 
[TXT]Agda.Builtin.Nat.html 12-Jul-2018 14:21 18K 
[TXT]Logical-equivalence...>12-Jul-2018 14:21 20K 
[TXT]Monad.Reader.html 12-Jul-2018 14:21 27K 
[TXT]Const.html 12-Jul-2018 14:21 30K 
[TXT]Vec.html 12-Jul-2018 14:21 35K 
[TXT]Vec.Data.html 12-Jul-2018 14:21 35K 
[TXT]Monad.State.html 12-Jul-2018 14:21 36K 
[TXT]Tree-sort.Partial.html 12-Jul-2018 14:21 38K 
[TXT]H-level.html 12-Jul-2018 14:21 39K 
[TXT]Double-negation.html 12-Jul-2018 14:21 40K 
[TXT]Groupoid.html 12-Jul-2018 14:21 46K 
[TXT]Surjection.html 12-Jul-2018 14:21 51K 
[TXT]Maybe.html 12-Jul-2018 14:21 51K 
[TXT]Omniscience.html 12-Jul-2018 14:21 51K 
[TXT]Container.Stream.html 12-Jul-2018 14:21 53K 
[TXT]Preimage.html 12-Jul-2018 14:21 59K 
[TXT]Container.Tree-sort...>12-Jul-2018 14:21 61K 
[TXT]Embedding.html 12-Jul-2018 14:21 62K 
[TXT]Tree.html 12-Jul-2018 14:21 62K 
[TXT]Adjunction.html 12-Jul-2018 14:21 65K 
[TXT]Bool.html 12-Jul-2018 14:21 66K 
[TXT]Circle.html 12-Jul-2018 14:21 68K 
[TXT]Equality.Decidable-U..>12-Jul-2018 14:21 70K 
[TXT]Nat.Eliminator.html 12-Jul-2018 14:21 73K 
[TXT]List.html 12-Jul-2018 14:21 78K 
[TXT]Agda.Builtin.Reflect..>12-Jul-2018 14:21 80K 
[TXT]Equality.Decision-pr..>12-Jul-2018 14:21 80K 
[TXT]Container.Tree.html 12-Jul-2018 14:21 92K 
[TXT]Record.html 12-Jul-2018 14:21 97K 
[TXT]Equality.Instances-r..>12-Jul-2018 14:21 103K 
[TXT]Equality.Groupoid.html 12-Jul-2018 14:21 104K 
[TXT]Tree-sort.Full.html 12-Jul-2018 14:21 105K 
[TXT]M.html 12-Jul-2018 14:21 113K 
[TXT]Structure-identity-p..>12-Jul-2018 14:21 116K 
[TXT]Reflection.html 12-Jul-2018 14:21 120K 
[TXT]Prelude.html 12-Jul-2018 14:21 125K 
[TXT]Monad.html 12-Jul-2018 14:21 126K 
[TXT]Container.List.html 12-Jul-2018 14:21 127K 
[TXT]Equality.Tactic.html 12-Jul-2018 14:21 143K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 144K 
[TXT]Bijection.html 12-Jul-2018 14:21 157K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 163K 
[TXT]Fin.html 12-Jul-2018 14:21 179K 
[TXT]Tactic.By.html 12-Jul-2018 14:21 183K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 223K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 227K 
[TXT]Container.html 12-Jul-2018 14:21 240K 
[TXT]Nat.html 12-Jul-2018 14:21 257K 
[TXT]Conat.html 12-Jul-2018 14:21 294K 
[TXT]H-level.Closure.html 12-Jul-2018 14:21 298K 
[TXT]Functor.html 12-Jul-2018 14:21 335K 
[TXT]Bag-equivalence.html 12-Jul-2018 14:21 366K 
[TXT]Quotient.html 12-Jul-2018 14:21 389K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 440K 
[TXT]Colist.html 12-Jul-2018 14:21 452K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 478K 
[TXT]H-level.Truncation.html12-Jul-2018 14:21 554K 
[TXT]Univalence-axiom.html 12-Jul-2018 14:21 567K 
[TXT]Equivalence.html 12-Jul-2018 14:21 652K 
[TXT]Category.html 12-Jul-2018 14:21 713K 
[TXT]Equality.html 12-Jul-2018 14:21 827K 
[TXT]Univalence-axiom.Iso..>12-Jul-2018 14:21 1.2M 
[TXT]Function-universe.html 12-Jul-2018 14:21 1.4M 

README
------------------------------------------------------------------------
-- Experiments related to equality
--
-- Nils Anders Danielsson
--
-- Some files have been developed in collaboration with others, see
-- the individual files.
------------------------------------------------------------------------

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

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 reader monad transformer.

import Monad.Reader

-- The state monad transformer.

import Monad.State

-- The double-negation monad.

import Double-negation

-- The univalence axiom.

import Univalence-axiom

-- Truncation.

import H-level.Truncation

-- The "circle".

import Circle

-- Some omniscience principles.

import Omniscience

-- Lists.

import List

-- Conatural numbers.

import Conat

-- Colists.

import Colist

-- 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, defined using a recursive function.

import Vec

-- Vectors, defined using an inductive family.

import Vec.Data

-- Some properties related to the const function.

import Const

-- Support for reflection.

import Reflection

-- Some tactics aimed at making equational reasoning proofs more
-- readable.

import Tactic.By

-- Quotients.

import Quotient

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