Index of /~nad/listings/partiality-monad

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Univalence-axiom.html 17-Oct-2017 19:08 565K 
[TXT]Surjection.html 17-Oct-2017 19:08 50K 
[TXT]Structure-identity-p..>17-Oct-2017 19:08 115K 
[TXT]Search.html 17-Oct-2017 19:08 29K 
[TXT]README.html 17-Oct-2017 19:08 13K 
[TXT]README.Pointers-to-r..>17-Oct-2017 19:08 32K 
[TXT]README.Lambda.html 17-Oct-2017 19:08 5.7K 
[TXT]Quotient.html 17-Oct-2017 19:08 388K 
[TXT]Quotient.HIT.html 17-Oct-2017 19:08 301K 
[TXT]Prelude.html 17-Oct-2017 19:08 124K 
[TXT]Preimage.html 17-Oct-2017 19:08 59K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 15K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 47K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 100K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 20K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 24K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 213K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 127K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 214K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 77K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 5.5K 
[TXT]Partiality-monad.Ind..>17-Oct-2017 19:08 330K 
[TXT]Partiality-monad.Equ..>17-Oct-2017 19:08 155K 
[TXT]Partiality-monad.Coi..>17-Oct-2017 19:08 5.3K 
[TXT]Partiality-monad.Coi..>17-Oct-2017 19:08 54K 
[TXT]Partiality-monad.Coi..>17-Oct-2017 19:08 16K 
[TXT]Partiality-algebra.html17-Oct-2017 19:08 104K 
[TXT]Partiality-algebra.S..>17-Oct-2017 19:08 47K 
[TXT]Partiality-algebra.P..>17-Oct-2017 19:08 112K 
[TXT]Partiality-algebra.P..>17-Oct-2017 19:08 43K 
[TXT]Partiality-algebra.O..>17-Oct-2017 19:08 48K 
[TXT]Partiality-algebra.M..>17-Oct-2017 19:08 53K 
[TXT]Partiality-algebra.F..>17-Oct-2017 19:08 112K 
[TXT]Partiality-algebra.E..>17-Oct-2017 19:08 243K 
[TXT]Partiality-algebra.C..>17-Oct-2017 19:08 219K 
[TXT]Omega-cpo.html 17-Oct-2017 19:08 43K 
[TXT]Nat.html 17-Oct-2017 19:08 84K 
[TXT]Monad.html 17-Oct-2017 19:08 124K 
[TXT]Maybe.html 17-Oct-2017 19:08 44K 
[TXT]Logical-equivalence...>17-Oct-2017 19:08 20K 
[TXT]List.html 17-Oct-2017 19:08 59K 
[TXT]Lifting.html 17-Oct-2017 19:08 71K 
[TXT]Lifting.Preliminary-..>17-Oct-2017 19:08 60K 
[TXT]Lifting.Partiality-m..>17-Oct-2017 19:08 52K 
[TXT]Lambda.Virtual-machi..>17-Oct-2017 19:08 25K 
[TXT]Lambda.Syntax.html 17-Oct-2017 19:08 46K 
[TXT]Lambda.Simplified.Vi..>17-Oct-2017 19:08 25K 
[TXT]Lambda.Simplified.Sy..>17-Oct-2017 19:08 12K 
[TXT]Lambda.Simplified.Pa..>17-Oct-2017 19:08 6.7K 
[TXT]Lambda.Simplified.Pa..>17-Oct-2017 19:08 119K 
[TXT]Lambda.Simplified.Pa..>17-Oct-2017 19:08 100K 
[TXT]Lambda.Simplified.De..>17-Oct-2017 19:08 5.4K 
[TXT]Lambda.Simplified.De..>17-Oct-2017 19:08 11K 
[TXT]Lambda.Simplified.De..>17-Oct-2017 19:08 67K 
[TXT]Lambda.Simplified.Co..>17-Oct-2017 19:08 13K 
[TXT]Lambda.Partiality-mo..>17-Oct-2017 19:08 13K 
[TXT]Lambda.Partiality-mo..>17-Oct-2017 19:08 47K 
[TXT]Lambda.Partiality-mo..>17-Oct-2017 19:08 104K 
[TXT]Lambda.Partiality-mo..>17-Oct-2017 19:08 104K 
[TXT]Lambda.Delay-monad.V..>17-Oct-2017 19:08 6.1K 
[TXT]Lambda.Delay-monad.T..>17-Oct-2017 19:08 29K 
[TXT]Lambda.Delay-monad.I..>17-Oct-2017 19:08 21K 
[TXT]Lambda.Delay-monad.C..>17-Oct-2017 19:08 95K 
[TXT]Lambda.Compiler.html 17-Oct-2017 19:08 13K 
[TXT]Interval.html 17-Oct-2017 19:08 74K 
[TXT]Injection.html 17-Oct-2017 19:08 17K 
[TXT]H-level.html 17-Oct-2017 19:08 38K 
[TXT]H-level.Truncation.html17-Oct-2017 19:08 552K 
[TXT]H-level.Truncation.P..>17-Oct-2017 19:08 197K 
[TXT]H-level.Closure.html 17-Oct-2017 19:08 292K 
[TXT]Groupoid.html 17-Oct-2017 19:08 45K 
[TXT]Functor.html 17-Oct-2017 19:08 333K 
[TXT]Function-universe.html 17-Oct-2017 19:08 1.4M 
[TXT]Fin.html 17-Oct-2017 19:08 87K 
[TXT]Equivalence.html 17-Oct-2017 19:08 647K 
[TXT]Equality.html 17-Oct-2017 19:08 819K 
[TXT]Equality.Tactic.html 17-Oct-2017 19:08 143K 
[TXT]Equality.Proposition..>17-Oct-2017 19:08 13K 
[TXT]Equality.Proposition..>17-Oct-2017 19:08 1.3K 
[TXT]Equality.Groupoid.html 17-Oct-2017 19:08 104K 
[TXT]Equality.Decision-pr..>17-Oct-2017 19:08 78K 
[TXT]Equality.Decidable-U..>17-Oct-2017 19:08 70K 
[TXT]Embedding.html 17-Oct-2017 19:08 62K 
[TXT]Double-negation.html 17-Oct-2017 19:08 37K 
[TXT]Delay-monad.html 17-Oct-2017 19:08 8.1K 
[TXT]Delay-monad.Weak-bis..>17-Oct-2017 19:08 303K 
[TXT]Delay-monad.Strong-b..>17-Oct-2017 19:08 44K 
[TXT]Delay-monad.Partial-..>17-Oct-2017 19:08 155K 
[TXT]Delay-monad.Monad.html 17-Oct-2017 19:08 61K 
[TXT]Delay-monad.Always.html17-Oct-2017 19:08 14K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 11K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 27K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 107K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 103K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 33K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 120K 
[TXT]Delay-monad.Alternat..>17-Oct-2017 19:08 167K 
[TXT]Category.html 17-Oct-2017 19:08 711K 
[TXT]Bool.html 17-Oct-2017 19:08 66K 
[TXT]Bijection.html 17-Oct-2017 19:08 156K 
[TXT]Agda.css 17-Oct-2017 19:08 1.2K 
[TXT]Agda.Primitive.html 17-Oct-2017 19:08 3.6K 
[TXT]Agda.Primitive.Cubic..>17-Oct-2017 19:08 14K 
[TXT]Agda.Builtin.Unit.html 17-Oct-2017 19:08 1.2K 
[TXT]Agda.Builtin.Size.html 17-Oct-2017 19:08 1.6K 
[TXT]Agda.Builtin.Nat.html 17-Oct-2017 19:08 17K 
[TXT]Agda.Builtin.List.html 17-Oct-2017 19:08 4.2K 
[TXT]Agda.Builtin.Equalit..>17-Oct-2017 19:08 2.2K 
[TXT]Agda.Builtin.Bool.html 17-Oct-2017 19:08 2.4K 
[TXT]Adjunction.html 17-Oct-2017 19:08 65K 

README
------------------------------------------------------------------------
-- Code related to the paper "Partiality, Revisited: The Partiality
-- Monad as a Quotient Inductive-Inductive Type"
--
-- Thorsten Altenkirch, Nils Anders Danielsson and Nicolai Kraus
------------------------------------------------------------------------

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

module README where

-- Note that our definition of the partiality monad and some of the
-- results are heavily inspired by the section on Cauchy reals in the
-- HoTT book (first edition).

-- The partiality algebra code uses ideas and concepts from "Inductive
-- types in homotopy type theory" by Awodey, Gambino and Sojakova,
-- "Inductive Types in Homotopy Type Theory" by Sojakova, "Quotient
-- inductive-inductive types" by Altenkirch, Capriotti, Dijkstra and
-- Nordvall Forsberg, and Gabe Dijkstra's forthcoming PhD thesis.

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Preliminaries

-- A partial inductive-recursive definition of the partiality monad,
-- without path or truncation constructors, in order to get the basics
-- right.

import Partiality-monad.Inductive.Preliminary-sketch

------------------------------------------------------------------------
-- Partiality algebras

-- Partiality algebras.

import Partiality-algebra

-- Some partiality algebra properties.

import Partiality-algebra.Properties

-- Partiality algebra categories.

import Partiality-algebra.Category

-- Eliminators and initiality.

import Partiality-algebra.Eliminators

-- Monotone functions.

import Partiality-algebra.Monotone

-- ω-continuous functions.

import Partiality-algebra.Omega-continuous

-- Strict ω-continuous functions.

import Partiality-algebra.Strict-omega-continuous

-- Fixpoint combinators.

import Partiality-algebra.Fixpoints

-- Pi with partiality algebra families as codomains.

import Partiality-algebra.Pi

------------------------------------------------------------------------
-- The partiality monad

-- A quotient inductive-inductive definition of the partiality monad.

import Partiality-monad.Inductive

-- Specialised eliminators.

import Partiality-monad.Inductive.Eliminators

-- A function that runs computations.

import Partiality-monad.Inductive.Approximate

-- An alternative characterisation of the information ordering, along
-- with related results.

import Partiality-monad.Inductive.Alternative-order

-- Monotone functions.

import Partiality-monad.Inductive.Monotone

-- ω-continuous functions.

import Partiality-monad.Inductive.Omega-continuous

-- The partiality monad's monad instance.

import Partiality-monad.Inductive.Monad

-- The partiality monad's monad instance, defined via an adjunction.

import Partiality-monad.Inductive.Monad.Adjunction

-- Strict ω-continuous functions.

import Partiality-monad.Inductive.Strict-omega-continuous

-- Fixpoint combinators.

import Partiality-monad.Inductive.Fixpoints

------------------------------------------------------------------------
-- Some examples

-- A function that, given a stream, tries to find an element
-- satisfying a predicate.

import Search

-- Examples involving simple λ-calculi.

import README.Lambda

------------------------------------------------------------------------
-- An alternative definition of the delay monad

-- The delay monad, defined using increasing sequences of potential
-- values.

import Delay-monad.Alternative

-- Various properties.

import Delay-monad.Alternative.Properties

-- Theorems relating the coinductive definition of the delay
-- monad to the alternative one and to another type.

import Delay-monad.Alternative.Equivalence

-- Termination predicates.

import Delay-monad.Alternative.Termination

-- Information orderings.

import Delay-monad.Alternative.Partial-order

-- Weak bisimilarity.

import Delay-monad.Alternative.Weak-bisimilarity

-- Two eliminators for Delay-monad.Alternative.Delay (A / R).

import Delay-monad.Alternative.Eliminators

------------------------------------------------------------------------
-- The delay monad quotiented by weak bisimilarity

-- The delay monad quotiented by weak bisimilarity.

import Partiality-monad.Coinductive

-- A partial order.

import Partiality-monad.Coinductive.Partial-order

-- An alternative definition of the partiality monad: a variant of the
-- delay monad quotiented by a notion of weak bisimilarity.

import Partiality-monad.Coinductive.Alternative

------------------------------------------------------------------------
-- A proof of equivalence

-- The partiality monads in Partiality-monad.Inductive and
-- Partiality-monad.Coinductive are pointwise equivalent, for sets,
-- assuming extensionality, propositional extensionality and countable
-- choice.

import Partiality-monad.Equivalence

------------------------------------------------------------------------
-- ω-cpos

-- Pointed and non-pointed ω-cpos.

import Omega-cpo

-- The code in the following three modules is based on a suggestion
-- from Paolo Capriotti.

-- A partial inductive-recursive definition of the lifting
-- construction on ω-cpos, without path or truncation constructors, in
-- order to get the basics right.

import Lifting.Preliminary-sketch

-- A quotient inductive-inductive definition of the lifting
-- construction on ω-cpos.

import Lifting

-- An alternative but equivalent definition of the partiality monad
-- (but only for sets), based on the lifting construction in Lifting.

import Lifting.Partiality-monad