Name | Last modified | Size | Description | |
---|---|---|---|---|

Parent Directory | - | |||

Agda.css | 17-Oct-2017 19:11 | 1.2K | ||

Agda.Builtin.Unit.html | 17-Oct-2017 19:11 | 1.2K | ||

Agda.Builtin.Size.html | 17-Oct-2017 19:11 | 1.6K | ||

README.Weak-J.html | 17-Oct-2017 19:11 | 1.8K | ||

Agda.Builtin.Equalit..> | 17-Oct-2017 19:11 | 2.2K | ||

Agda.Builtin.Bool.html | 17-Oct-2017 19:11 | 2.4K | ||

Agda.Builtin.Int.html | 17-Oct-2017 19:11 | 3.0K | ||

Agda.Builtin.Char.html | 17-Oct-2017 19:11 | 3.3K | ||

Agda.Primitive.html | 17-Oct-2017 19:11 | 3.6K | ||

Agda.Builtin.List.html | 17-Oct-2017 19:11 | 4.2K | ||

Agda.Builtin.String...> | 17-Oct-2017 19:11 | 5.0K | ||

Container.Tree-sort...> | 17-Oct-2017 19:11 | 7.4K | ||

Agda.Builtin.Float.html | 17-Oct-2017 19:11 | 9.2K | ||

README.Isomorphism-i..> | 17-Oct-2017 19:11 | 10K | ||

README.Bag-equivalen..> | 17-Oct-2017 19:11 | 11K | ||

Tree-sort.Examples.html | 17-Oct-2017 19:11 | 11K | ||

Equality.Proposition..> | 17-Oct-2017 19:11 | 13K | ||

Agda.Primitive.Cubic..> | 17-Oct-2017 19:11 | 14K | ||

README.html | 17-Oct-2017 19:11 | 15K | ||

Injection.html | 17-Oct-2017 19:11 | 17K | ||

Agda.Builtin.Nat.html | 17-Oct-2017 19:11 | 17K | ||

Logical-equivalence...> | 17-Oct-2017 19:11 | 20K | ||

Monad.Reader.html | 17-Oct-2017 19:11 | 26K | ||

Vec.html | 17-Oct-2017 19:11 | 29K | ||

Const.html | 17-Oct-2017 19:11 | 30K | ||

Monad.State.html | 17-Oct-2017 19:11 | 36K | ||

Double-negation.html | 17-Oct-2017 19:11 | 37K | ||

Tree-sort.Partial.html | 17-Oct-2017 19:11 | 37K | ||

H-level.html | 17-Oct-2017 19:11 | 38K | ||

Maybe.html | 17-Oct-2017 19:11 | 44K | ||

Groupoid.html | 17-Oct-2017 19:11 | 45K | ||

Surjection.html | 17-Oct-2017 19:11 | 50K | ||

Container.Stream.html | 17-Oct-2017 19:11 | 53K | ||

Preimage.html | 17-Oct-2017 19:11 | 59K | ||

List.html | 17-Oct-2017 19:11 | 59K | ||

Container.Tree-sort...> | 17-Oct-2017 19:11 | 61K | ||

Embedding.html | 17-Oct-2017 19:11 | 62K | ||

Tree.html | 17-Oct-2017 19:11 | 62K | ||

Adjunction.html | 17-Oct-2017 19:11 | 65K | ||

Bool.html | 17-Oct-2017 19:11 | 66K | ||

Circle.html | 17-Oct-2017 19:11 | 68K | ||

Equality.Decidable-U..> | 17-Oct-2017 19:11 | 70K | ||

Nat.Eliminator.html | 17-Oct-2017 19:11 | 73K | ||

Agda.Builtin.Reflect..> | 17-Oct-2017 19:11 | 77K | ||

Equality.Decision-pr..> | 17-Oct-2017 19:11 | 78K | ||

Nat.html | 17-Oct-2017 19:11 | 84K | ||

Fin.html | 17-Oct-2017 19:11 | 87K | ||

Container.Tree.html | 17-Oct-2017 19:11 | 91K | ||

M.html | 17-Oct-2017 19:11 | 93K | ||

Record.html | 17-Oct-2017 19:11 | 96K | ||

Equality.Instances-r..> | 17-Oct-2017 19:11 | 103K | ||

Tree-sort.Full.html | 17-Oct-2017 19:11 | 104K | ||

Equality.Groupoid.html | 17-Oct-2017 19:11 | 104K | ||

Reflection.html | 17-Oct-2017 19:11 | 113K | ||

Structure-identity-p..> | 17-Oct-2017 19:11 | 115K | ||

Tactic.By.html | 17-Oct-2017 19:11 | 116K | ||

Monad.html | 17-Oct-2017 19:11 | 124K | ||

Prelude.html | 17-Oct-2017 19:11 | 124K | ||

Container.List.html | 17-Oct-2017 19:11 | 127K | ||

Equality.Tactic.html | 17-Oct-2017 19:11 | 143K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 144K | ||

Bijection.html | 17-Oct-2017 19:11 | 156K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 169K | ||

Container.html | 17-Oct-2017 19:11 | 215K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 222K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 226K | ||

H-level.Closure.html | 17-Oct-2017 19:11 | 292K | ||

Functor.html | 17-Oct-2017 19:11 | 333K | ||

Bag-equivalence.html | 17-Oct-2017 19:11 | 344K | ||

Quotient.html | 17-Oct-2017 19:11 | 388K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 435K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 477K | ||

H-level.Truncation.html | 17-Oct-2017 19:11 | 552K | ||

Univalence-axiom.html | 17-Oct-2017 19:11 | 565K | ||

Equivalence.html | 17-Oct-2017 19:11 | 647K | ||

Category.html | 17-Oct-2017 19:11 | 711K | ||

Equality.html | 17-Oct-2017 19:11 | 819K | ||

Univalence-axiom.Iso..> | 17-Oct-2017 19:11 | 1.2M | ||

Function-universe.html | 17-Oct-2017 19:11 | 1.4M | ||

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