![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| Accessibility.html | 2023-09-29 17:40 | 94K | |
| Agda.Builtin.Bool.html | 2023-09-29 17:40 | 3.1K | |
| Agda.Builtin.Char.html | 2023-09-29 17:40 | 4.0K | |
| Agda.Builtin.Cubical..> | 2023-09-29 17:40 | 3.2K | |
| Agda.Builtin.Cubical..> | 2023-09-29 17:40 | 5.1K | |
| Agda.Builtin.Equalit..> | 2023-09-29 17:40 | 2.6K | |
| Agda.Builtin.Int.html | 2023-09-29 17:40 | 3.4K | |
| Agda.Builtin.List.html | 2023-09-29 17:40 | 4.7K | |
| Agda.Builtin.Maybe.html | 2023-09-29 17:40 | 2.3K | |
| Agda.Builtin.Nat.html | 2023-09-29 17:40 | 23K | |
| Agda.Builtin.Sigma.html | 2023-09-29 17:40 | 3.4K | |
| Agda.Builtin.Size.html | 2023-09-29 17:40 | 4.2K | |
| Agda.Builtin.String...> | 2023-09-29 17:40 | 10K | |
| Agda.Builtin.Unit.html | 2023-09-29 17:40 | 1.7K | |
| Agda.Primitive.Cubic..> | 2023-09-29 17:40 | 24K | |
| Agda.Primitive.html | 2023-09-29 17:40 | 5.4K | |
| Agda.css | 2023-09-29 17:40 | 1.8K | |
| Algebra.Bundles.Raw...> | 2023-09-29 17:40 | 54K | |
| Algebra.Bundles.html | 2023-09-29 17:40 | 255K | |
| Algebra.Consequences..> | 2023-09-29 17:40 | 7.1K | |
| Algebra.Consequences..> | 2023-09-29 17:40 | 39K | |
| Algebra.Consequences..> | 2023-09-29 17:40 | 165K | |
| Algebra.Construct.Li..> | 2023-09-29 17:40 | 83K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 17K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 7.3K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 18K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 13K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 57K | |
| Algebra.Construct.Na..> | 2023-09-29 17:40 | 109K | |
| Algebra.Core.html | 2023-09-29 17:40 | 3.3K | |
| Algebra.Definitions...> | 2023-09-29 17:40 | 16K | |
| Algebra.Definitions...> | 2023-09-29 17:40 | 11K | |
| Algebra.Definitions...> | 2023-09-29 17:40 | 21K | |
| Algebra.Definitions...> | 2023-09-29 17:40 | 118K | |
| Algebra.Lattice.Bund..> | 2023-09-29 17:40 | 7.2K | |
| Algebra.Lattice.Bund..> | 2023-09-29 17:40 | 51K | |
| Algebra.Lattice.Cons..> | 2023-09-29 17:40 | 4.5K | |
| Algebra.Lattice.Cons..> | 2023-09-29 17:40 | 18K | |
| Algebra.Lattice.Cons..> | 2023-09-29 17:40 | 6.3K | |
| Algebra.Lattice.Prop..> | 2023-09-29 17:40 | 293K | |
| Algebra.Lattice.Prop..> | 2023-09-29 17:40 | 6.0K | |
| Algebra.Lattice.Prop..> | 2023-09-29 17:40 | 42K | |
| Algebra.Lattice.Prop..> | 2023-09-29 17:40 | 11K | |
| Algebra.Lattice.Stru..> | 2023-09-29 17:40 | 41K | |
| Algebra.Morphism.Def..> | 2023-09-29 17:40 | 11K | |
| Algebra.Morphism.Str..> | 2023-09-29 17:40 | 177K | |
| Algebra.Morphism.html | 2023-09-29 17:40 | 47K | |
| Algebra.Properties.A..> | 2023-09-29 17:40 | 12K | |
| Algebra.Properties.C..> | 2023-09-29 17:40 | 112K | |
| Algebra.Properties.G..> | 2023-09-29 17:40 | 52K | |
| Algebra.Properties.M..> | 2023-09-29 17:40 | 30K | |
| Algebra.Properties.R..> | 2023-09-29 17:40 | 41K | |
| Algebra.Properties.S..> | 2023-09-29 17:40 | 8.2K | |
| Algebra.Properties.S..> | 2023-09-29 17:40 | 38K | |
| Algebra.Solver.Ring...> | 2023-09-29 17:40 | 43K | |
| Algebra.Solver.Ring...> | 2023-09-29 17:40 | 96K | |
| Algebra.Solver.Ring...> | 2023-09-29 17:40 | 4.3K | |
| Algebra.Solver.Ring...> | 2023-09-29 17:40 | 294K | |
| Algebra.Structures.B..> | 2023-09-29 17:40 | 64K | |
| Algebra.Structures.html | 2023-09-29 17:40 | 210K | |
| Algebra.html | 2023-09-29 17:40 | 1.9K | |
| Axiom.Extensionality..> | 2023-09-29 17:40 | 21K | |
| Axiom.UniquenessOfId..> | 2023-09-29 17:40 | 23K | |
| Bijection.html | 2023-09-29 17:40 | 226K | |
| Bool.html | 2023-09-29 17:40 | 74K | |
| Conat.html | 2023-09-29 17:40 | 432K | |
| Data.Bool.Base.html | 2023-09-29 17:40 | 13K | |
| Data.Bool.Properties..> | 2023-09-29 17:40 | 204K | |
| Data.Empty.Irrelevan..> | 2023-09-29 17:40 | 2.2K | |
| Data.Empty.Polymorph..> | 2023-09-29 17:40 | 3.8K | |
| Data.Empty.html | 2023-09-29 17:40 | 4.1K | |
| Data.Fin.Base.html | 2023-09-29 17:40 | 117K | |
| Data.Fin.Patterns.html | 2023-09-29 17:40 | 4.3K | |
| Data.Fin.Properties...> | 2023-09-29 17:40 | 540K | |
| Data.Irrelevant.html | 2023-09-29 17:40 | 12K | |
| Data.List.Base.html | 2023-09-29 17:40 | 194K | |
| Data.List.Effectful...> | 2023-09-29 17:40 | 142K | |
| Data.List.Extrema.Co..> | 2023-09-29 17:40 | 60K | |
| Data.List.Extrema.html | 2023-09-29 17:40 | 132K | |
| Data.List.Membership..> | 2023-09-29 17:40 | 36K | |
| Data.List.Membership..> | 2023-09-29 17:40 | 202K | |
| Data.List.Membership..> | 2023-09-29 17:40 | 9.3K | |
| Data.List.Membership..> | 2023-09-29 17:40 | 227K | |
| Data.List.Membership..> | 2023-09-29 17:40 | 19K | |
| Data.List.Properties..> | 2023-09-29 17:40 | 618K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 6.3K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 48K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 26K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 37K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 127K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 2.8K | |
| Data.List.Relation.B..> | 2023-09-29 17:40 | 10K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 411K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 110K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 6.3K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 36K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 452K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 38K | |
| Data.List.Relation.U..> | 2023-09-29 17:40 | 5.7K | |
| Data.Maybe.Base.html | 2023-09-29 17:40 | 37K | |
| Data.Maybe.Relation...> | 2023-09-29 17:40 | 54K | |
| Data.Maybe.Relation...> | 2023-09-29 17:40 | 31K | |
| Data.Nat.Base.html | 2023-09-29 17:40 | 83K | |
| Data.Nat.DivMod.Core..> | 2023-09-29 17:40 | 222K | |
| Data.Nat.DivMod.html | 2023-09-29 17:40 | 363K | |
| Data.Nat.Divisibilit..> | 2023-09-29 17:40 | 15K | |
| Data.Nat.Divisibilit..> | 2023-09-29 17:40 | 158K | |
| Data.Nat.Induction.html | 2023-09-29 17:40 | 25K | |
| Data.Nat.Properties...> | 2023-09-29 17:40 | 908K | |
| Data.Nat.Solver.html | 2023-09-29 17:40 | 2.4K | |
| Data.Nat.html | 2023-09-29 17:40 | 5.7K | |
| Data.Parity.Base.html | 2023-09-29 17:40 | 19K | |
| Data.Product.Algebra..> | 2023-09-29 17:40 | 52K | |
| Data.Product.Base.html | 2023-09-29 17:40 | 87K | |
| Data.Product.Functio..> | 2023-09-29 17:40 | 159K | |
| Data.Product.Functio..> | 2023-09-29 17:40 | 36K | |
| Data.Product.Functio..> | 2023-09-29 17:40 | 55K | |
| Data.Product.Propert..> | 2023-09-29 17:40 | 55K | |
| Data.Product.Relatio..> | 2023-09-29 17:40 | 113K | |
| Data.Product.Relatio..> | 2023-09-29 17:40 | 5.4K | |
| Data.Sign.Base.html | 2023-09-29 17:40 | 8.9K | |
| Data.Sum.Algebra.html | 2023-09-29 17:40 | 30K | |
| Data.Sum.Base.html | 2023-09-29 17:40 | 26K | |
| Data.Sum.Function.Pr..> | 2023-09-29 17:40 | 34K | |
| Data.Sum.Function.Se..> | 2023-09-29 17:40 | 56K | |
| Data.Sum.Properties...> | 2023-09-29 17:40 | 60K | |
| Data.Sum.Relation.Bi..> | 2023-09-29 17:40 | 111K | |
| Data.These.Base.html | 2023-09-29 17:40 | 36K | |
| Data.Unit.Base.html | 2023-09-29 17:40 | 1.9K | |
| Data.Unit.Polymorphi..> | 2023-09-29 17:40 | 3.3K | |
| Data.Unit.Polymorphi..> | 2023-09-29 17:40 | 23K | |
| Data.Unit.Polymorphi..> | 2023-09-29 17:40 | 1.9K | |
| Data.Unit.Properties..> | 2023-09-29 17:40 | 16K | |
| Data.Unit.html | 2023-09-29 17:40 | 1.7K | |
| Data.Vec.Base.html | 2023-09-29 17:40 | 153K | |
| Data.Vec.Bounded.Bas..> | 2023-09-29 17:40 | 68K | |
| Data.Vec.Functional...> | 2023-09-29 17:40 | 69K | |
| Data.Vec.N-ary.html | 2023-09-29 17:40 | 92K | |
| Data.Vec.html | 2023-09-29 17:40 | 12K | |
| Delay-monad.Always.html | 2023-09-29 17:40 | 14K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 57K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 92K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 9.0K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 195K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 140K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 135K | |
| Delay-monad.Bisimila..> | 2023-09-29 17:40 | 246K | |
| Delay-monad.Least-up..> | 2023-09-29 17:40 | 76K | |
| Delay-monad.Monad.html | 2023-09-29 17:40 | 61K | |
| Delay-monad.Parallel..> | 2023-09-29 17:40 | 137K | |
| Delay-monad.Partial-..> | 2023-09-29 17:40 | 158K | |
| Delay-monad.Quantita..> | 2023-09-29 17:40 | 426K | |
| Delay-monad.Sequenti..> | 2023-09-29 17:40 | 104K | |
| Delay-monad.Sized.Al..> | 2023-09-29 17:40 | 16K | |
| Delay-monad.Sized.Bi..> | 2023-09-29 17:40 | 60K | |
| Delay-monad.Sized.Bi..> | 2023-09-29 17:40 | 97K | |
| Delay-monad.Sized.Bi..> | 2023-09-29 17:40 | 211K | |
| Delay-monad.Sized.Bi..> | 2023-09-29 17:40 | 235K | |
| Delay-monad.Sized.Le..> | 2023-09-29 17:40 | 80K | |
| Delay-monad.Sized.Mo..> | 2023-09-29 17:40 | 55K | |
| Delay-monad.Sized.Pa..> | 2023-09-29 17:40 | 172K | |
| Delay-monad.Sized.Te..> | 2023-09-29 17:40 | 45K | |
| Delay-monad.Sized.html | 2023-09-29 17:40 | 15K | |
| Delay-monad.Terminat..> | 2023-09-29 17:40 | 42K | |
| Delay-monad.html | 2023-09-29 17:40 | 16K | |
| Double-negation.html | 2023-09-29 17:40 | 96K | |
| Effect.Applicative.html | 2023-09-29 17:40 | 36K | |
| Effect.Choice.html | 2023-09-29 17:40 | 4.4K | |
| Effect.Empty.html | 2023-09-29 17:40 | 3.4K | |
| Effect.Functor.html | 2023-09-29 17:40 | 13K | |
| Effect.Monad.html | 2023-09-29 17:40 | 32K | |
| Embedding.html | 2023-09-29 17:40 | 82K | |
| Equality.Decidable-U..> | 2023-09-29 17:40 | 76K | |
| Equality.Decision-pr..> | 2023-09-29 17:40 | 97K | |
| Equality.Instances-r..> | 2023-09-29 17:40 | 120K | |
| Equality.Path.html | 2023-09-29 17:40 | 342K | |
| Equality.Proposition..> | 2023-09-29 17:40 | 19K | |
| Equality.html | 2023-09-29 17:40 | 1.0M | |
| Equivalence-relation..> | 2023-09-29 17:40 | 82K | |
| Equivalence.Contract..> | 2023-09-29 17:40 | 128K | |
| Equivalence.Erased.B..> | 2023-09-29 17:40 | 97K | |
| Equivalence.Erased.C..> | 2023-09-29 17:40 | 70K | |
| Equivalence.Half-adj..> | 2023-09-29 17:40 | 133K | |
| Equivalence.List.html | 2023-09-29 17:40 | 355K | |
| Equivalence.Path-spl..> | 2023-09-29 17:40 | 413K | |
| Equivalence.html | 2023-09-29 17:40 | 502K | |
| Erased.Basics.html | 2023-09-29 17:40 | 14K | |
| Erased.Box-cong-axio..> | 2023-09-29 17:40 | 7.0K | |
| Erased.Level-1.html | 2023-09-29 17:40 | 1.0M | |
| Excluded-middle.html | 2023-09-29 17:40 | 6.6K | |
| Extensionality.html | 2023-09-29 17:40 | 189K | |
| For-iterated-equalit..> | 2023-09-29 17:40 | 337K | |
| Function-universe.html | 2023-09-29 17:40 | 2.5M | |
| Function.Base.html | 2023-09-29 17:40 | 75K | |
| Function.Bijection.html | 2023-09-29 17:40 | 33K | |
| Function.Bundles.html | 2023-09-29 17:40 | 110K | |
| Function.Consequence..> | 2023-09-29 17:40 | 22K | |
| Function.Consequence..> | 2023-09-29 17:40 | 34K | |
| Function.Construct.C..> | 2023-09-29 17:40 | 115K | |
| Function.Construct.I..> | 2023-09-29 17:40 | 45K | |
| Function.Construct.S..> | 2023-09-29 17:40 | 72K | |
| Function.Core.html | 2023-09-29 17:40 | 5.0K | |
| Function.Definitions..> | 2023-09-29 17:40 | 21K | |
| Function.Equality.html | 2023-09-29 17:40 | 40K | |
| Function.Equivalence..> | 2023-09-29 17:40 | 40K | |
| Function.HalfAdjoint..> | 2023-09-29 17:40 | 46K | |
| Function.Injection.html | 2023-09-29 17:40 | 23K | |
| Function.Inverse.html | 2023-09-29 17:40 | 60K | |
| Function.LeftInverse..> | 2023-09-29 17:40 | 42K | |
| Function.Metric.Bund..> | 2023-09-29 17:40 | 37K | |
| Function.Metric.Core..> | 2023-09-29 17:40 | 2.8K | |
| Function.Metric.Defi..> | 2023-09-29 17:40 | 35K | |
| Function.Metric.Nat...> | 2023-09-29 17:40 | 28K | |
| Function.Metric.Nat...> | 2023-09-29 17:40 | 2.6K | |
| Function.Metric.Nat...> | 2023-09-29 17:40 | 17K | |
| Function.Metric.Nat...> | 2023-09-29 17:40 | 18K | |
| Function.Metric.Nat...> | 2023-09-29 17:40 | 1.8K | |
| Function.Metric.Stru..> | 2023-09-29 17:40 | 22K | |
| Function.Properties...> | 2023-09-29 17:40 | 20K | |
| Function.Properties...> | 2023-09-29 17:40 | 28K | |
| Function.Properties...> | 2023-09-29 17:40 | 7.7K | |
| Function.Properties...> | 2023-09-29 17:40 | 13K | |
| Function.Related.Pro..> | 2023-09-29 17:40 | 126K | |
| Function.Related.Typ..> | 2023-09-29 17:40 | 185K | |
| Function.Related.html | 2023-09-29 17:40 | 163K | |
| Function.Structures...> | 2023-09-29 17:40 | 43K | |
| Function.Surjection...> | 2023-09-29 17:40 | 33K | |
| Groupoid.html | 2023-09-29 17:40 | 189K | |
| H-level.Closure.html | 2023-09-29 17:40 | 406K | |
| H-level.html | 2023-09-29 17:40 | 53K | |
| Induction.WellFounde..> | 2023-09-29 17:40 | 87K | |
| Induction.html | 2023-09-29 17:40 | 17K | |
| Injection.html | 2023-09-29 17:40 | 18K | |
| Integer.Basics.html | 2023-09-29 17:40 | 40K | |
| Level.html | 2023-09-29 17:40 | 5.6K | |
| List.html | 2023-09-29 17:40 | 265K | |
| Logical-equivalence...> | 2023-09-29 17:40 | 50K | |
| Modality.Basics.html | 2023-09-29 17:40 | 2.1M | |
| Monad.Raw.html | 2023-09-29 17:40 | 18K | |
| Monad.html | 2023-09-29 17:40 | 115K | |
| Nat.Solver.html | 2023-09-29 17:40 | 59K | |
| Nat.html | 2023-09-29 17:40 | 476K | |
| Preimage.html | 2023-09-29 17:40 | 59K | |
| Prelude.Size.html | 2023-09-29 17:40 | 3.1K | |
| Prelude.html | 2023-09-29 17:40 | 123K | |
| Pullback.html | 2023-09-29 17:40 | 102K | |
| Relation.Binary.Bund..> | 2023-09-29 17:40 | 66K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 101K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 72K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 78K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 77K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 69K | |
| Relation.Binary.Cons..> | 2023-09-29 17:40 | 83K | |
| Relation.Binary.Core..> | 2023-09-29 17:40 | 19K | |
| Relation.Binary.Defi..> | 2023-09-29 17:40 | 91K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 11K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 15K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 13K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 10K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 13K | |
| Relation.Binary.Inde..> | 2023-09-29 17:40 | 2.1K | |
| Relation.Binary.Latt..> | 2023-09-29 17:40 | 68K | |
| Relation.Binary.Latt..> | 2023-09-29 17:40 | 12K | |
| Relation.Binary.Latt..> | 2023-09-29 17:40 | 61K | |
| Relation.Binary.Latt..> | 2023-09-29 17:40 | 1.7K | |
| Relation.Binary.Morp..> | 2023-09-29 17:40 | 6.3K | |
| Relation.Binary.Morp..> | 2023-09-29 17:40 | 38K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 15K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 34K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 9.8K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 18K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 17K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 5.5K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 45K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 104K | |
| Relation.Binary.Prop..> | 2023-09-29 17:40 | 53K | |
| Relation.Binary.Reas..> | 2023-09-29 17:40 | 45K | |
| Relation.Binary.Reas..> | 2023-09-29 17:40 | 20K | |
| Relation.Binary.Reas..> | 2023-09-29 17:40 | 69K | |
| Relation.Binary.Reas..> | 2023-09-29 17:40 | 3.5K | |
| Relation.Binary.Reas..> | 2023-09-29 17:40 | 7.4K | |
| Relation.Binary.Refl..> | 2023-09-29 17:40 | 37K | |
| Relation.Binary.Stru..> | 2023-09-29 17:40 | 62K | |
| Relation.Binary.html | 2023-09-29 17:40 | 1.9K | |
| Relation.Nullary.Dec..> | 2023-09-29 17:40 | 56K | |
| Relation.Nullary.Dec..> | 2023-09-29 17:40 | 32K | |
| Relation.Nullary.Ind..> | 2023-09-29 17:40 | 3.2K | |
| Relation.Nullary.Neg..> | 2023-09-29 17:40 | 21K | |
| Relation.Nullary.Neg..> | 2023-09-29 17:40 | 38K | |
| Relation.Nullary.Ref..> | 2023-09-29 17:40 | 34K | |
| Relation.Nullary.html | 2023-09-29 17:40 | 6.5K | |
| Relation.Unary.Prope..> | 2023-09-29 17:40 | 113K | |
| Relation.Unary.html | 2023-09-29 17:40 | 91K | |
| Surjection.html | 2023-09-29 17:40 | 88K | |
| Univalence-axiom.html | 2023-09-29 17:40 | 706K | |
| Vec.Dependent.html | 2023-09-29 17:40 | 47K | |
------------------------------------------------------------------------
-- Code related to the delay monad
--
-- Nils Anders Danielsson
------------------------------------------------------------------------
{-# OPTIONS --cubical --sized-types #-}
module README where
-- The concept referred to as the delay monad here is the monad
-- presented by Capretta in "General Recursion via Coinductive Types".
------------------------------------------------------------------------
-- The delay monad
-- The delay monad, defined coinductively.
import Delay-monad
-- A type used to index a combined definition of strong and weak
-- bisimilarity and expansion.
import Delay-monad.Bisimilarity.Kind
-- A combined definition of strong and weak bisimilarity and
-- expansion, along with various properties.
import Delay-monad.Bisimilarity
-- Strong bisimilarity for partially defined values, along with a
-- proof showing that this relation is pointwise isomorphic to path
-- equality.
import Delay-monad.Bisimilarity.For-all-sizes
-- A variant of weak bisimilarity that can be used to relate the
-- number of steps in two computations.
import Delay-monad.Quantitative-weak-bisimilarity
-- Termination.
import Delay-monad.Termination
-- Alternative definitions of weak bisimilarity.
import Delay-monad.Bisimilarity.Alternative
-- An observation about weak bisimilarity.
import Delay-monad.Bisimilarity.Observation
-- Some negative results related to weak bisimilarity and expansion.
import Delay-monad.Bisimilarity.Negative
-- An example showing that transitivity-like proofs that are not
-- size-preserving can sometimes be used in a compositional way.
import Delay-monad.Bisimilarity.Transitivity-constructor
-- A partial order.
import Delay-monad.Partial-order
-- Least upper bounds.
import Delay-monad.Least-upper-bound
-- The delay monad is a monad up to strong bisimilarity.
import Delay-monad.Monad
-- The "always true" predicate, □.
import Delay-monad.Always
-- A combinator for running two (independent) computations in
-- sequence.
import Delay-monad.Sequential
-- A combinator for running two computations in parallel.
import Delay-monad.Parallel
------------------------------------------------------------------------
-- A variant of the delay monad with a sized type parameter
-- The delay monad, defined coinductively, with a sized type
-- parameter.
import Delay-monad.Sized
-- A combined definition of strong and weak bisimilarity and
-- expansion, along with various properties.
import Delay-monad.Sized.Bisimilarity
-- Strong bisimilarity for partially defined values, along with a
-- proof showing that this relation is pointwise isomorphic to path
-- equality.
import Delay-monad.Sized.Bisimilarity.For-all-sizes
-- Termination.
import Delay-monad.Sized.Termination
-- Alternative definitions of weak bisimilarity.
import Delay-monad.Sized.Bisimilarity.Alternative
-- Some negative results related to weak bisimilarity and expansion.
import Delay-monad.Sized.Bisimilarity.Negative
-- A partial order.
import Delay-monad.Sized.Partial-order
-- Least upper bounds.
import Delay-monad.Sized.Least-upper-bound
-- A monad-like structure.
import Delay-monad.Sized.Monad
-- The "always true" predicate, □.
import Delay-monad.Sized.Always