Index of /~nad/listings/partiality-monad

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.css 10-Sep-2018 10:44 1.2K 
[TXT]Agda.Builtin.Unit.html 10-Sep-2018 10:44 1.2K 
[TXT]Equality.Proposition..>10-Sep-2018 10:44 1.3K 
[TXT]Agda.Builtin.Equalit..>10-Sep-2018 10:44 2.3K 
[TXT]Agda.Builtin.Bool.html 10-Sep-2018 10:44 2.4K 
[TXT]Agda.Builtin.Size.html 10-Sep-2018 10:44 2.9K 
[TXT]Agda.Builtin.List.html 10-Sep-2018 10:44 3.6K 
[TXT]Agda.Primitive.html 10-Sep-2018 10:44 3.6K 
[TXT]Partiality-monad.Coi..>10-Sep-2018 10:44 5.4K 
[TXT]Lambda.Simplified.De..>10-Sep-2018 10:44 5.4K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 5.5K 
[TXT]README.Lambda.html 10-Sep-2018 10:44 5.7K 
[TXT]Lambda.Delay-monad.V..>10-Sep-2018 10:44 6.1K 
[TXT]Lambda.Simplified.Pa..>10-Sep-2018 10:44 6.8K 
[TXT]Delay-monad.Bisimila..>10-Sep-2018 10:44 9.0K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 11K 
[TXT]Lambda.Simplified.De..>10-Sep-2018 10:44 11K 
[TXT]Lambda.Simplified.Sy..>10-Sep-2018 10:44 12K 
[TXT]Lambda.Simplified.Co..>10-Sep-2018 10:44 13K 
[TXT]Equality.Proposition..>10-Sep-2018 10:44 13K 
[TXT]README.html 10-Sep-2018 10:44 13K 
[TXT]Lambda.Compiler.html 10-Sep-2018 10:44 13K 
[TXT]Lambda.Partiality-mo..>10-Sep-2018 10:44 13K 
[TXT]Delay-monad.html 10-Sep-2018 10:44 14K 
[TXT]Delay-monad.Always.html10-Sep-2018 10:44 14K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 16K 
[TXT]Partiality-monad.Coi..>10-Sep-2018 10:44 16K 
[TXT]Injection.html 10-Sep-2018 10:44 17K 
[TXT]Agda.Builtin.Nat.html 10-Sep-2018 10:44 18K 
[TXT]Logical-equivalence...>10-Sep-2018 10:44 20K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 20K 
[TXT]Lambda.Delay-monad.I..>10-Sep-2018 10:44 21K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 24K 
[TXT]Lambda.Simplified.Vi..>10-Sep-2018 10:44 25K 
[TXT]Lambda.Virtual-machi..>10-Sep-2018 10:44 25K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 27K 
[TXT]Lambda.Delay-monad.T..>10-Sep-2018 10:44 29K 
[TXT]Search.html 10-Sep-2018 10:44 29K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 33K 
[TXT]README.Pointers-to-r..>10-Sep-2018 10:44 34K 
[TXT]H-level.html 10-Sep-2018 10:44 39K 
[TXT]Double-negation.html 10-Sep-2018 10:44 40K 
[TXT]Delay-monad.Terminat..>10-Sep-2018 10:44 42K 
[TXT]Partiality-algebra.P..>10-Sep-2018 10:44 43K 
[TXT]Omega-cpo.html 10-Sep-2018 10:44 43K 
[TXT]Groupoid.html 10-Sep-2018 10:44 46K 
[TXT]Lambda.Syntax.html 10-Sep-2018 10:44 47K 
[TXT]Lambda.Partiality-mo..>10-Sep-2018 10:44 47K 
[TXT]Delay-monad.Monad.html 10-Sep-2018 10:44 47K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 47K 
[TXT]Partiality-algebra.S..>10-Sep-2018 10:44 47K 
[TXT]Partiality-algebra.O..>10-Sep-2018 10:44 48K 
[TXT]Surjection.html 10-Sep-2018 10:44 51K 
[TXT]Maybe.html 10-Sep-2018 10:44 51K 
[TXT]Lifting.Partiality-m..>10-Sep-2018 10:44 53K 
[TXT]Partiality-algebra.M..>10-Sep-2018 10:44 53K 
[TXT]Partiality-monad.Coi..>10-Sep-2018 10:44 54K 
[TXT]Delay-monad.Bisimila..>10-Sep-2018 10:44 57K 
[TXT]Preimage.html 10-Sep-2018 10:44 59K 
[TXT]Lifting.Preliminary-..>10-Sep-2018 10:44 61K 
[TXT]Embedding.html 10-Sep-2018 10:44 62K 
[TXT]Adjunction.html 10-Sep-2018 10:44 65K 
[TXT]Bool.html 10-Sep-2018 10:44 66K 
[TXT]Lambda.Simplified.De..>10-Sep-2018 10:44 67K 
[TXT]Equality.Decidable-U..>10-Sep-2018 10:44 70K 
[TXT]Lifting.html 10-Sep-2018 10:44 72K 
[TXT]Interval.html 10-Sep-2018 10:44 75K 
[TXT]List.html 10-Sep-2018 10:44 78K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 78K 
[TXT]Equality.Decision-pr..>10-Sep-2018 10:44 80K 
[TXT]Lambda.Delay-monad.C..>10-Sep-2018 10:44 94K 
[TXT]Lambda.Simplified.Pa..>10-Sep-2018 10:44 100K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 101K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 103K 
[TXT]Equality.Groupoid.html 10-Sep-2018 10:44 104K 
[TXT]Lambda.Partiality-mo..>10-Sep-2018 10:44 105K 
[TXT]Lambda.Partiality-mo..>10-Sep-2018 10:44 105K 
[TXT]Partiality-algebra.html10-Sep-2018 10:44 106K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 107K 
[TXT]Partiality-algebra.F..>10-Sep-2018 10:44 112K 
[TXT]Partiality-algebra.P..>10-Sep-2018 10:44 113K 
[TXT]Structure-identity-p..>10-Sep-2018 10:44 116K 
[TXT]Lambda.Simplified.Pa..>10-Sep-2018 10:44 120K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 120K 
[TXT]Prelude.html 10-Sep-2018 10:44 125K 
[TXT]Monad.html 10-Sep-2018 10:44 126K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 127K 
[TXT]Equality.Tactic.html 10-Sep-2018 10:44 143K 
[TXT]Partiality-monad.Equ..>10-Sep-2018 10:44 155K 
[TXT]Delay-monad.Partial-..>10-Sep-2018 10:44 156K 
[TXT]Bijection.html 10-Sep-2018 10:44 157K 
[TXT]Delay-monad.Alternat..>10-Sep-2018 10:44 167K 
[TXT]Fin.html 10-Sep-2018 10:44 179K 
[TXT]Delay-monad.Bisimila..>10-Sep-2018 10:44 193K 
[TXT]H-level.Truncation.P..>10-Sep-2018 10:44 198K 
[TXT]Delay-monad.Bisimila..>10-Sep-2018 10:44 208K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 214K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 214K 
[TXT]Partiality-algebra.C..>10-Sep-2018 10:44 220K 
[TXT]Partiality-algebra.E..>10-Sep-2018 10:44 244K 
[TXT]Nat.html 10-Sep-2018 10:44 257K 
[TXT]H-level.Closure.html 10-Sep-2018 10:44 298K 
[TXT]Quotient.HIT.html 10-Sep-2018 10:44 302K 
[TXT]Partiality-monad.Ind..>10-Sep-2018 10:44 332K 
[TXT]Functor.html 10-Sep-2018 10:44 335K 
[TXT]Quotient.html 10-Sep-2018 10:44 389K 
[TXT]H-level.Truncation.html10-Sep-2018 10:44 554K 
[TXT]Univalence-axiom.html 10-Sep-2018 10:44 567K 
[TXT]Equivalence.html 10-Sep-2018 10:44 652K 
[TXT]Category.html 10-Sep-2018 10:44 713K 
[TXT]Equality.html 10-Sep-2018 10:44 827K 
[TXT]Function-universe.html 10-Sep-2018 10:44 1.4M 

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