------------------------------------------------------------------------
-- Safe modules that use --cubical-compatible
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical-compatible #-}

module README.Safe.Cubical-compatible where

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

import Prelude

-- Logical equivalences.

import Logical-equivalence

-- Some definitions related to Dec.

import Dec

-- 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 was that I thought that I might
-- later want to use a definition of equality where the application
-- elim P r (refl x) did not compute to r x, unlike the equality in
-- Equality.Propositional. Now, with the advent of cubical type theory
-- and paths, there is such an equality (see Equality.Path).
--
-- (Note that Equality.Tactic contains a definition of equality which,
-- roughly speaking, computes like the one in Equality.Propositional.)

import Equality

-- One model of the axioms: propositional equality.

import Equality.Propositional

-- A simple tactic for proving equality of equality proofs.

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

-- Types with decidable equality have unique identity proofs, and
-- related results.

import Equality.Decidable-UIP

-- Some decision procedures for equality.

import Equality.Decision-procedures

-- Bijections.

import Bijection

-- Integers.

import Integer.Basics

-- Groupoids.

import Groupoid

-- Preimages.

import Preimage

-- Is-equivalence, defined in terms of contractible fibres.

import Equivalence.Contractible-preimages

-- Half adjoint equivalences.

import Equivalence.Half-adjoint

-- Function extensionality.

import Extensionality

-- Closure properties for h-levels.

import H-level.Closure

-- Excluded middle.

import Excluded-middle

-- Equivalence relations

import Equivalence-relation

-- Equivalences.

import Equivalence

-- A type for values that should be erased at run-time.

import Erased.Basics

-- An axiomatisation for []-cong.

import Erased.Box-cong-axiomatisation

-- Equivalences with erased "proofs", defined in terms of partly
-- erased contractible fibres.

import Equivalence.Erased.Contractible-preimages.Basics

-- Equivalences with erased "proofs".

import Equivalence.Erased.Basics

-- Embeddings.

import Embedding

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

import Function-universe

-- The accessibility predicate.

import Accessibility

-- Pullbacks.

import Pullback

-- Some alternative definitions of the concept of being an
-- equivalence.

import Equivalence.Path-split

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

-- A solver for certain natural number equalities.

import Nat.Solver

-- Some definitions related to the binary sum type former.

import Sum

-- Some definitions related to and properties of booleans.

import Bool

-- Raw monads.

import Monad.Raw

-- Monads.

import Monad

-- The reader monad transformer.

import Monad.Reader

-- The state monad transformer.

import Monad.State

-- Lists.

import List

-- Vectors for which the element types depend on the position, defined
-- using a recursive function.

import Vec.Dependent

-- Some results related to the For-iterated-equality predicate
-- transformer.

import For-iterated-equality

-- Lists of equivalent types.

import Equivalence.List

-- The univalence axiom.

import Univalence-axiom

-- Idempotent monadic modalities.

import Modality.Basics

-- Some results that hold for left exact modalities.

import Modality.Left-exact

-- The identity modality.

import Modality.Identity

-- A type for values that should be erased at run-time.

import Erased.Level-1

-- The double-negation monad.

import Double-negation

-- Pointed types and loop spaces.

import Pointed-type

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

import Equality.Groupoid

-- Groups.

import Group

-- Integers.

import Integer

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

import Fin

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

-- Vectors, defined as functions from finite sets.

import Vec.Function

-- Some properties related to the const function.

import Const

-- Support for reflection.

import TC-monad

-- Tactics for proving instances of Σ-cong (and Surjection.Σ-cong)
-- with "better" computational behaviour.

import Tactic.Sigma-cong

-- Code used to construct tactics aimed at making equational reasoning
-- proofs more readable.

import Tactic.By

-- A tactic aimed at making equational reasoning proofs more readable
-- in modules that are parametrised by an implementation of equality.

import Tactic.By.Parametrised
import Tactic.By.Parametrised.Tests

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

import Tactic.By.Propositional

-- Equivalences with erased "proofs", defined in terms of partly
-- erased contractible fibres.

import Equivalence.Erased.Contractible-preimages

-- Equivalences with erased "proofs".

import Equivalence.Erased

-- Embeddings with erased "proofs".

import Embedding.Erased

-- A type for values that should be erased at run-time.

import Erased.Level-2

-- Some results related to modalities that hold if the []-cong axioms
-- can be instantiated.

import Modality.Box-cong

-- Some results that hold for modalities that satisfy a choice
-- principle.

import Modality.Has-choice

-- Some results that hold for modalities that commute with Erased.

import Modality.Commutes-with-Erased

-- Some results that hold for every very modal modality.

import Modality.Very-modal

-- Some results that hold for every empty-modal modality.

import Modality.Empty-modal

-- Idempotent monadic modalities.

import Modality

-- The zero modality.

import Modality.Zero

-- Properties related to stability for Erased.

import Erased.Stability

-- Truncation, defined using a kind of Church encoding.

import H-level.Truncation.Church

-- Some omniscience principles.

import Omniscience

-- Bag equivalence for lists.

import Bag-equivalence

-- The All predicate, defined using _∈_.

import List.All

-- The All predicate, defined recursively.

import List.All.Recursive

-- Quotients, defined as families of equivalence classes.

import Quotient.Families-of-equivalence-classes

-- A type for values that should be erased at run-time.

import Erased
import Erased.Without-box-cong

-- A wrapper that turns a representation of natural numbers (with a
-- unique representative for every number) into a representation that
-- computes roughly like the unary natural numbers (at least for some
-- operations).

import Nat.Wrapper

-- A binary representation of natural numbers.

import Nat.Binary

-- Specifications of output-restricted deques (single-ended queues
-- with cons).

import Queue

-- Simple queues, implemented in the usual way using two lists
-- (following Hood and Melville).

import Queue.Simple

-- Queue instances for the queues in Queue.Simple.

import Queue.Simple.Instances

-- Banker's queues (following Okasaki).

import Queue.Bankers

-- Queue instances for the queues in Queue.Bankers.

import Queue.Bankers.Instances

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

-- Bi-invertibility.

import Bi-invertibility
import Bi-invertibility.Erased

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

-- Indexed containers.

import Container.Indexed

-- Coalgebras for indexed containers.

import Container.Indexed.Coalgebra

-- Algebras for indexed containers.

import Container.Indexed.Algebra

-- Another definition of indexed containers.

import Container.Indexed.Variant

-- Coalgebras for the indexed containers in Container.Indexed.Variant.

import Container.Indexed.Variant.Coalgebra

-- Algebras for the indexed containers in Container.Indexed.Variant.

import Container.Indexed.Variant.Algebra

-- M-types for indexed containers, defined using functions.

import Container.Indexed.M.Function

-- Record types with manifest fields and "with".

import Records-with-with

-- Overview of code related to some papers.

import README.Bag-equivalence
import README.Isomorphism-is-equality
import README.Weak-J