![[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 | 2025-05-12 09:11 | 94K | |
| Agda.Builtin.Bool.html | 2025-05-12 09:11 | 3.1K | |
| Agda.Builtin.Char.html | 2025-05-12 09:11 | 4.0K | |
| Agda.Builtin.Equalit..> | 2025-05-12 09:11 | 2.6K | |
| Agda.Builtin.Int.html | 2025-05-12 09:11 | 3.4K | |
| Agda.Builtin.List.html | 2025-05-12 09:11 | 4.7K | |
| Agda.Builtin.Maybe.html | 2025-05-12 09:11 | 2.3K | |
| Agda.Builtin.Nat.html | 2025-05-12 09:11 | 23K | |
| Agda.Builtin.Sigma.html | 2025-05-12 09:11 | 3.4K | |
| Agda.Builtin.Size.html | 2025-05-12 09:11 | 4.2K | |
| Agda.Builtin.String...> | 2025-05-12 09:11 | 10K | |
| Agda.Builtin.Unit.html | 2025-05-12 09:11 | 1.7K | |
| Agda.Primitive.html | 2025-05-12 09:11 | 5.4K | |
| Agda.css | 2025-05-12 09:11 | 1.8K | |
| Algebra.Bundles.Raw...> | 2025-05-12 09:11 | 66K | |
| Algebra.Bundles.html | 2025-05-12 09:11 | 282K | |
| Algebra.Consequences..> | 2025-05-12 09:11 | 9.5K | |
| Algebra.Consequences..> | 2025-05-12 09:11 | 48K | |
| Algebra.Consequences..> | 2025-05-12 09:11 | 179K | |
| Algebra.Construct.Li..> | 2025-05-12 09:11 | 84K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 17K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 7.5K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 18K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 13K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 56K | |
| Algebra.Construct.Na..> | 2025-05-12 09:11 | 109K | |
| Algebra.Core.html | 2025-05-12 09:11 | 3.3K | |
| Algebra.Definitions...> | 2025-05-12 09:11 | 19K | |
| Algebra.Definitions...> | 2025-05-12 09:11 | 11K | |
| Algebra.Definitions...> | 2025-05-12 09:11 | 21K | |
| Algebra.Definitions...> | 2025-05-12 09:11 | 118K | |
| Algebra.Lattice.Bund..> | 2025-05-12 09:11 | 7.4K | |
| Algebra.Lattice.Bund..> | 2025-05-12 09:11 | 53K | |
| Algebra.Lattice.Cons..> | 2025-05-12 09:11 | 4.8K | |
| Algebra.Lattice.Cons..> | 2025-05-12 09:11 | 19K | |
| Algebra.Lattice.Cons..> | 2025-05-12 09:11 | 6.5K | |
| Algebra.Lattice.Prop..> | 2025-05-12 09:11 | 292K | |
| Algebra.Lattice.Prop..> | 2025-05-12 09:11 | 6.2K | |
| Algebra.Lattice.Prop..> | 2025-05-12 09:11 | 43K | |
| Algebra.Lattice.Prop..> | 2025-05-12 09:11 | 11K | |
| Algebra.Lattice.Stru..> | 2025-05-12 09:11 | 40K | |
| Algebra.Morphism.Def..> | 2025-05-12 09:11 | 11K | |
| Algebra.Morphism.Str..> | 2025-05-12 09:11 | 210K | |
| Algebra.Morphism.html | 2025-05-12 09:11 | 47K | |
| Algebra.Properties.A..> | 2025-05-12 09:11 | 13K | |
| Algebra.Properties.C..> | 2025-05-12 09:11 | 112K | |
| Algebra.Properties.G..> | 2025-05-12 09:11 | 70K | |
| Algebra.Properties.L..> | 2025-05-12 09:11 | 21K | |
| Algebra.Properties.M..> | 2025-05-12 09:11 | 32K | |
| Algebra.Properties.Q..> | 2025-05-12 09:11 | 17K | |
| Algebra.Properties.R..> | 2025-05-12 09:11 | 6.4K | |
| Algebra.Properties.R..> | 2025-05-12 09:11 | 44K | |
| Algebra.Properties.S..> | 2025-05-12 09:11 | 8.2K | |
| Algebra.Properties.S..> | 2025-05-12 09:11 | 39K | |
| Algebra.Solver.Ring...> | 2025-05-12 09:11 | 45K | |
| Algebra.Solver.Ring...> | 2025-05-12 09:11 | 96K | |
| Algebra.Solver.Ring...> | 2025-05-12 09:11 | 4.6K | |
| Algebra.Solver.Ring...> | 2025-05-12 09:11 | 288K | |
| Algebra.Structures.B..> | 2025-05-12 09:11 | 65K | |
| Algebra.Structures.html | 2025-05-12 09:11 | 233K | |
| Algebra.html | 2025-05-12 09:11 | 1.9K | |
| Axiom.Extensionality..> | 2025-05-12 09:11 | 21K | |
| Axiom.UniquenessOfId..> | 2025-05-12 09:11 | 21K | |
| Bijection.html | 2025-05-12 09:11 | 226K | |
| Bisimilarity.6-2-5.html | 2025-05-12 09:11 | 94K | |
| Bisimilarity.CCS.Cla..> | 2025-05-12 09:11 | 96K | |
| Bisimilarity.CCS.Exa..> | 2025-05-12 09:11 | 61K | |
| Bisimilarity.CCS.Exa..> | 2025-05-12 09:11 | 62K | |
| Bisimilarity.CCS.Exa..> | 2025-05-12 09:11 | 451K | |
| Bisimilarity.CCS.Gen..> | 2025-05-12 09:11 | 86K | |
| Bisimilarity.CCS.html | 2025-05-12 09:11 | 364K | |
| Bisimilarity.Classic..> | 2025-05-12 09:11 | 5.0K | |
| Bisimilarity.Classic..> | 2025-05-12 09:11 | 132K | |
| Bisimilarity.Compari..> | 2025-05-12 09:11 | 79K | |
| Bisimilarity.Delay-m..> | 2025-05-12 09:11 | 21K | |
| Bisimilarity.Equatio..> | 2025-05-12 09:11 | 19K | |
| Bisimilarity.General..> | 2025-05-12 09:11 | 108K | |
| Bisimilarity.Step.html | 2025-05-12 09:11 | 68K | |
| Bisimilarity.Up-to.C..> | 2025-05-12 09:11 | 115K | |
| Bisimilarity.Up-to.C..> | 2025-05-12 09:11 | 311K | |
| Bisimilarity.Up-to.html | 2025-05-12 09:11 | 22K | |
| Bisimilarity.Weak.Al..> | 2025-05-12 09:11 | 4.2K | |
| Bisimilarity.Weak.Al..> | 2025-05-12 09:11 | 47K | |
| Bisimilarity.Weak.Al..> | 2025-05-12 09:11 | 14K | |
| Bisimilarity.Weak.Al..> | 2025-05-12 09:11 | 30K | |
| Bisimilarity.Weak.Al..> | 2025-05-12 09:11 | 19K | |
| Bisimilarity.Weak.CC..> | 2025-05-12 09:11 | 274K | |
| Bisimilarity.Weak.CC..> | 2025-05-12 09:11 | 198K | |
| Bisimilarity.Weak.De..> | 2025-05-12 09:11 | 157K | |
| Bisimilarity.Weak.Eq..> | 2025-05-12 09:11 | 85K | |
| Bisimilarity.Weak.Eq..> | 2025-05-12 09:11 | 24K | |
| Bisimilarity.Weak.Up..> | 2025-05-12 09:11 | 67K | |
| Bisimilarity.Weak.Up..> | 2025-05-12 09:11 | 96K | |
| Bisimilarity.Weak.html | 2025-05-12 09:11 | 92K | |
| Bisimilarity.html | 2025-05-12 09:11 | 55K | |
| Bool.html | 2025-05-12 09:11 | 74K | |
| Conat.html | 2025-05-12 09:11 | 432K | |
| Data.Bool.Base.html | 2025-05-12 09:11 | 13K | |
| Data.Bool.ListAction..> | 2025-05-12 09:11 | 7.3K | |
| Data.Bool.Properties..> | 2025-05-12 09:11 | 207K | |
| Data.Empty.Polymorph..> | 2025-05-12 09:11 | 4.5K | |
| Data.Empty.html | 2025-05-12 09:11 | 5.0K | |
| Data.Fin.Base.html | 2025-05-12 09:11 | 114K | |
| Data.Fin.Patterns.html | 2025-05-12 09:11 | 4.7K | |
| Data.Fin.Properties...> | 2025-05-12 09:11 | 547K | |
| Data.Irrelevant.html | 2025-05-12 09:11 | 12K | |
| Data.List.Base.html | 2025-05-12 09:11 | 223K | |
| Data.List.Effectful...> | 2025-05-12 09:11 | 147K | |
| Data.List.Extrema.Co..> | 2025-05-12 09:11 | 62K | |
| Data.List.Extrema.html | 2025-05-12 09:11 | 132K | |
| Data.List.Membership..> | 2025-05-12 09:11 | 44K | |
| Data.List.Membership..> | 2025-05-12 09:11 | 239K | |
| Data.List.Membership..> | 2025-05-12 09:11 | 9.3K | |
| Data.List.Membership..> | 2025-05-12 09:11 | 261K | |
| Data.List.Membership..> | 2025-05-12 09:11 | 20K | |
| Data.List.Properties..> | 2025-05-12 09:11 | 867K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 6.9K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 51K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 31K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 37K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 132K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 2.8K | |
| Data.List.Relation.B..> | 2025-05-12 09:11 | 11K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 49K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 388K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 112K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 6.3K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 36K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 459K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 38K | |
| Data.List.Relation.U..> | 2025-05-12 09:11 | 3.8K | |
| Data.Maybe.Base.html | 2025-05-12 09:11 | 37K | |
| Data.Maybe.Relation...> | 2025-05-12 09:11 | 56K | |
| Data.Maybe.Relation...> | 2025-05-12 09:11 | 33K | |
| Data.Nat.Base.html | 2025-05-12 09:11 | 103K | |
| Data.Nat.DivMod.Core..> | 2025-05-12 09:11 | 224K | |
| Data.Nat.DivMod.html | 2025-05-12 09:11 | 356K | |
| Data.Nat.Divisibilit..> | 2025-05-12 09:11 | 16K | |
| Data.Nat.Divisibilit..> | 2025-05-12 09:11 | 170K | |
| Data.Nat.Generalised..> | 2025-05-12 09:11 | 68K | |
| Data.Nat.Induction.html | 2025-05-12 09:11 | 25K | |
| Data.Nat.Properties...> | 2025-05-12 09:11 | 938K | |
| Data.Nat.Solver.html | 2025-05-12 09:11 | 2.4K | |
| Data.Parity.Base.html | 2025-05-12 09:11 | 19K | |
| Data.Product.Algebra..> | 2025-05-12 09:11 | 55K | |
| Data.Product.Base.html | 2025-05-12 09:11 | 87K | |
| Data.Product.Functio..> | 2025-05-12 09:11 | 163K | |
| Data.Product.Functio..> | 2025-05-12 09:11 | 49K | |
| Data.Product.Functio..> | 2025-05-12 09:11 | 59K | |
| Data.Product.Propert..> | 2025-05-12 09:11 | 57K | |
| Data.Product.Relatio..> | 2025-05-12 09:11 | 97K | |
| Data.Product.Relatio..> | 2025-05-12 09:11 | 5.4K | |
| Data.Sign.Base.html | 2025-05-12 09:11 | 8.9K | |
| Data.Sum.Algebra.html | 2025-05-12 09:11 | 33K | |
| Data.Sum.Base.html | 2025-05-12 09:11 | 26K | |
| Data.Sum.Function.Pr..> | 2025-05-12 09:11 | 46K | |
| Data.Sum.Function.Se..> | 2025-05-12 09:11 | 73K | |
| Data.Sum.Properties...> | 2025-05-12 09:11 | 60K | |
| Data.Sum.Relation.Bi..> | 2025-05-12 09:11 | 106K | |
| Data.Sum.html | 2025-05-12 09:11 | 12K | |
| Data.These.Base.html | 2025-05-12 09:11 | 37K | |
| Data.Unit.Base.html | 2025-05-12 09:11 | 1.9K | |
| Data.Unit.Polymorphi..> | 2025-05-12 09:11 | 3.6K | |
| Data.Unit.Polymorphi..> | 2025-05-12 09:11 | 27K | |
| Data.Unit.Polymorphi..> | 2025-05-12 09:11 | 1.9K | |
| Data.Vec.Base.html | 2025-05-12 09:11 | 150K | |
| Data.Vec.Bounded.Bas..> | 2025-05-12 09:11 | 68K | |
| Data.Vec.Functional...> | 2025-05-12 09:11 | 67K | |
| Data.Vec.N-ary.html | 2025-05-12 09:11 | 92K | |
| Data.Vec.html | 2025-05-12 09:11 | 12K | |
| Delay-monad.Bisimila..> | 2025-05-12 09:11 | 57K | |
| Delay-monad.Bisimila..> | 2025-05-12 09:11 | 9.0K | |
| Delay-monad.Bisimila..> | 2025-05-12 09:11 | 195K | |
| Delay-monad.Bisimila..> | 2025-05-12 09:11 | 246K | |
| Delay-monad.Partial-..> | 2025-05-12 09:11 | 158K | |
| Delay-monad.Terminat..> | 2025-05-12 09:11 | 42K | |
| Delay-monad.html | 2025-05-12 09:11 | 16K | |
| Double-negation.html | 2025-05-12 09:11 | 96K | |
| Effect.Applicative.html | 2025-05-12 09:11 | 36K | |
| Effect.Choice.html | 2025-05-12 09:11 | 4.4K | |
| Effect.Empty.html | 2025-05-12 09:11 | 3.8K | |
| Effect.Functor.html | 2025-05-12 09:11 | 13K | |
| Effect.Monad.html | 2025-05-12 09:11 | 35K | |
| Embedding.html | 2025-05-12 09:11 | 93K | |
| Equality.Decidable-U..> | 2025-05-12 09:11 | 76K | |
| Equality.Decision-pr..> | 2025-05-12 09:11 | 97K | |
| Equality.Groupoid.html | 2025-05-12 09:11 | 100K | |
| Equality.Instances-r..> | 2025-05-12 09:11 | 120K | |
| Equality.Proposition..> | 2025-05-12 09:11 | 19K | |
| Equality.Tactic.html | 2025-05-12 09:11 | 129K | |
| Equality.html | 2025-05-12 09:11 | 1.0M | |
| Equational-reasoning..> | 2025-05-12 09:11 | 73K | |
| Equivalence-relation..> | 2025-05-12 09:11 | 82K | |
| Equivalence.Contract..> | 2025-05-12 09:11 | 128K | |
| Equivalence.Erased.B..> | 2025-05-12 09:11 | 97K | |
| Equivalence.Erased.C..> | 2025-05-12 09:11 | 71K | |
| Equivalence.Half-adj..> | 2025-05-12 09:11 | 133K | |
| Equivalence.List.html | 2025-05-12 09:11 | 355K | |
| Equivalence.Path-spl..> | 2025-05-12 09:11 | 413K | |
| Equivalence.html | 2025-05-12 09:11 | 502K | |
| Erased.Basics.html | 2025-05-12 09:11 | 14K | |
| Erased.Box-cong-axio..> | 2025-05-12 09:11 | 7.0K | |
| Erased.Level-1.html | 2025-05-12 09:11 | 1.2M | |
| Excluded-middle.html | 2025-05-12 09:11 | 6.6K | |
| Expansion.CCS.html | 2025-05-12 09:11 | 339K | |
| Expansion.Delay-mona..> | 2025-05-12 09:11 | 85K | |
| Expansion.Equational..> | 2025-05-12 09:11 | 44K | |
| Expansion.html | 2025-05-12 09:11 | 103K | |
| Extensionality.html | 2025-05-12 09:11 | 189K | |
| Fin.html | 2025-05-12 09:11 | 183K | |
| For-iterated-equalit..> | 2025-05-12 09:11 | 337K | |
| Function-universe.Si..> | 2025-05-12 09:11 | 28K | |
| Function-universe.html | 2025-05-12 09:11 | 2.6M | |
| Function.Base.html | 2025-05-12 09:11 | 76K | |
| Function.Bundles.html | 2025-05-12 09:11 | 128K | |
| Function.Consequence..> | 2025-05-12 09:11 | 12K | |
| Function.Consequence..> | 2025-05-12 09:11 | 23K | |
| Function.Consequence..> | 2025-05-12 09:11 | 35K | |
| Function.Construct.C..> | 2025-05-12 09:11 | 119K | |
| Function.Construct.I..> | 2025-05-12 09:11 | 46K | |
| Function.Construct.S..> | 2025-05-12 09:11 | 72K | |
| Function.Core.html | 2025-05-12 09:11 | 5.0K | |
| Function.Definitions..> | 2025-05-12 09:11 | 21K | |
| Function.Dependent.B..> | 2025-05-12 09:11 | 9.3K | |
| Function.Indexed.Rel..> | 2025-05-12 09:11 | 8.2K | |
| Function.Metric.Bund..> | 2025-05-12 09:11 | 37K | |
| Function.Metric.Core..> | 2025-05-12 09:11 | 2.8K | |
| Function.Metric.Defi..> | 2025-05-12 09:11 | 35K | |
| Function.Metric.Nat...> | 2025-05-12 09:11 | 29K | |
| Function.Metric.Nat...> | 2025-05-12 09:11 | 2.8K | |
| Function.Metric.Nat...> | 2025-05-12 09:11 | 18K | |
| Function.Metric.Nat...> | 2025-05-12 09:11 | 19K | |
| Function.Metric.Nat...> | 2025-05-12 09:11 | 1.8K | |
| Function.Metric.Stru..> | 2025-05-12 09:11 | 22K | |
| Function.Properties...> | 2025-05-12 09:11 | 21K | |
| Function.Properties...> | 2025-05-12 09:11 | 46K | |
| Function.Properties...> | 2025-05-12 09:11 | 53K | |
| Function.Properties...> | 2025-05-12 09:11 | 19K | |
| Function.Properties...> | 2025-05-12 09:11 | 23K | |
| Function.Related.Pro..> | 2025-05-12 09:11 | 120K | |
| Function.Related.Typ..> | 2025-05-12 09:11 | 165K | |
| Function.Structures...> | 2025-05-12 09:11 | 47K | |
| Groupoid.html | 2025-05-12 09:11 | 189K | |
| H-level.Closure.html | 2025-05-12 09:11 | 406K | |
| H-level.html | 2025-05-12 09:11 | 53K | |
| Indexed-container.Co..> | 2025-05-12 09:11 | 593K | |
| Indexed-container.De..> | 2025-05-12 09:11 | 62K | |
| Indexed-container.html | 2025-05-12 09:11 | 265K | |
| Induction.WellFounde..> | 2025-05-12 09:11 | 96K | |
| Induction.html | 2025-05-12 09:11 | 14K | |
| Injection.html | 2025-05-12 09:11 | 18K | |
| Integer.Basics.html | 2025-05-12 09:11 | 40K | |
| Labelled-transition-..> | 2025-05-12 09:11 | 17K | |
| Labelled-transition-..> | 2025-05-12 09:11 | 352K | |
| Labelled-transition-..> | 2025-05-12 09:11 | 119K | |
| Labelled-transition-..> | 2025-05-12 09:11 | 104K | |
| Labelled-transition-..> | 2025-05-12 09:11 | 238K | |
| Level.html | 2025-05-12 09:11 | 5.6K | |
| List.html | 2025-05-12 09:11 | 265K | |
| Logical-equivalence...> | 2025-05-12 09:11 | 50K | |
| Modality.Basics.html | 2025-05-12 09:11 | 2.1M | |
| Monad.Raw.html | 2025-05-12 09:11 | 18K | |
| Monad.html | 2025-05-12 09:11 | 115K | |
| Nat.Solver.html | 2025-05-12 09:11 | 59K | |
| Nat.html | 2025-05-12 09:11 | 476K | |
| Pointed-type.html | 2025-05-12 09:11 | 198K | |
| Preimage.html | 2025-05-12 09:11 | 59K | |
| Prelude.Size.html | 2025-05-12 09:11 | 3.1K | |
| Prelude.html | 2025-05-12 09:11 | 123K | |
| Pullback.html | 2025-05-12 09:11 | 102K | |
| Relation.Binary.Bund..> | 2025-05-12 09:11 | 12K | |
| Relation.Binary.Bund..> | 2025-05-12 09:11 | 98K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 101K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 50K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 77K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 82K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 80K | |
| Relation.Binary.Cons..> | 2025-05-12 09:11 | 73K | |
| Relation.Binary.Core..> | 2025-05-12 09:11 | 19K | |
| Relation.Binary.Defi..> | 2025-05-12 09:11 | 98K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 12K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 17K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 13K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 11K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 14K | |
| Relation.Binary.Inde..> | 2025-05-12 09:11 | 2.1K | |
| Relation.Binary.Latt..> | 2025-05-12 09:11 | 69K | |
| Relation.Binary.Latt..> | 2025-05-12 09:11 | 13K | |
| Relation.Binary.Latt..> | 2025-05-12 09:11 | 63K | |
| Relation.Binary.Latt..> | 2025-05-12 09:11 | 1.7K | |
| Relation.Binary.Morp..> | 2025-05-12 09:11 | 6.3K | |
| Relation.Binary.Morp..> | 2025-05-12 09:11 | 38K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 16K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 34K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 11K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 24K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 18K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 7.0K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 37K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 110K | |
| Relation.Binary.Prop..> | 2025-05-12 09:11 | 51K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 32K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 14K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 54K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 3.7K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 5.4K | |
| Relation.Binary.Reas..> | 2025-05-12 09:11 | 90K | |
| Relation.Binary.Refl..> | 2025-05-12 09:11 | 37K | |
| Relation.Binary.Stru..> | 2025-05-12 09:11 | 10K | |
| Relation.Binary.Stru..> | 2025-05-12 09:11 | 68K | |
| Relation.Binary.html | 2025-05-12 09:11 | 2.1K | |
| Relation.Nullary.Dec..> | 2025-05-12 09:11 | 69K | |
| Relation.Nullary.Dec..> | 2025-05-12 09:11 | 39K | |
| Relation.Nullary.Ind..> | 2025-05-12 09:11 | 3.2K | |
| Relation.Nullary.Neg..> | 2025-05-12 09:11 | 21K | |
| Relation.Nullary.Neg..> | 2025-05-12 09:11 | 38K | |
| Relation.Nullary.Rec..> | 2025-05-12 09:11 | 20K | |
| Relation.Nullary.Ref..> | 2025-05-12 09:11 | 42K | |
| Relation.Nullary.html | 2025-05-12 09:11 | 6.3K | |
| Relation.Unary.Predi..> | 2025-05-12 09:11 | 44K | |
| Relation.Unary.Prope..> | 2025-05-12 09:11 | 123K | |
| Relation.Unary.html | 2025-05-12 09:11 | 93K | |
| Relation.html | 2025-05-12 09:11 | 218K | |
| Similarity.CCS.html | 2025-05-12 09:11 | 133K | |
| Similarity.Equationa..> | 2025-05-12 09:11 | 24K | |
| Similarity.General.html | 2025-05-12 09:11 | 47K | |
| Similarity.Step.html | 2025-05-12 09:11 | 332K | |
| Similarity.Weak.Equa..> | 2025-05-12 09:11 | 48K | |
| Similarity.Weak.Up-t..> | 2025-05-12 09:11 | 10K | |
| Similarity.Weak.html | 2025-05-12 09:11 | 49K | |
| Similarity.html | 2025-05-12 09:11 | 29K | |
| Surjection.html | 2025-05-12 09:11 | 88K | |
| Univalence-axiom.html | 2025-05-12 09:11 | 706K | |
| Up-to.Closure.html | 2025-05-12 09:11 | 110K | |
| Up-to.Via.html | 2025-05-12 09:11 | 83K | |
| Up-to.html | 2025-05-12 09:11 | 300K | |
| Vec.Dependent.html | 2025-05-12 09:11 | 47K | |
------------------------------------------------------------------------
-- Code related to the paper "Up-to Techniques using Sized Types"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------
{-# OPTIONS --sized-types #-}
module README where
------------------------------------------------------------------------
-- 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
------------------------------------------------------------------------
-- Some preliminaries
-- Overloaded "equational" reasoning combinators.
import Equational-reasoning
-- Unary and binary relations.
import Relation
------------------------------------------------------------------------
-- Containers
-- Indexed containers.
import Indexed-container
-- Container combinators.
import Indexed-container.Combinators
-- The delay monad defined as the greatest fixpoint of an indexed
-- container.
import Indexed-container.Delay-monad
------------------------------------------------------------------------
-- Up-to techniques
-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion.
import Up-to
-- Closure properties for Compatible and Size-preserving.
--
-- (Some negative results in this module depend on code presented
-- further down.)
import Up-to.Closure
-- Up-to techniques via.
import Up-to.Via
------------------------------------------------------------------------
-- Labelled transition systems
-- Labelled transition systems (LTSs).
import Labelled-transition-system
import Labelled-transition-system.Equational-reasoning-instances
-- CCS.
import Labelled-transition-system.CCS
-- A labelled transition system for the delay monad.
import Labelled-transition-system.Delay-monad
-- An LTS from Section 6.2.5 of "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi.
import Labelled-transition-system.6-2-5
------------------------------------------------------------------------
-- Similarity
-- The one-sided Step function, used to define similarity and the
-- two-sided Step function.
import Similarity.Step
-- A parametrised coinductive definition that can be used to define
-- various forms of similarity.
import Similarity.General
-- For more information about similarity, see "Similarity, continued"
-- below.
------------------------------------------------------------------------
-- Strong bisimilarity
-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion.
import Bisimilarity.Step
-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion.
import Bisimilarity.General
-- A coinductive definition of (strong) bisimilarity.
import Bisimilarity
import Bisimilarity.Equational-reasoning-instances
-- The classical definition of (strong) bisimilarity.
import Bisimilarity.Classical
import Bisimilarity.Classical.Equational-reasoning-instances
-- A comparison of the two definitions of bisimilarity.
import Bisimilarity.Comparison
-- Some results related to strong bisimilarity for the delay monad.
import Bisimilarity.Delay-monad
-- Some results related to CCS, implemented without using a fixed form
-- of bisimilarity.
import Bisimilarity.CCS.General
-- Various results or examples related to CCS, implemented using the
-- coinductive definition of bisimilarity.
import Bisimilarity.CCS
import Bisimilarity.CCS.Examples
import Bisimilarity.CCS.Examples.Natural-numbers
-- Some of the results/examples above have also been implemented using
-- the classical definition of bisimilarity.
import Bisimilarity.CCS.Classical
import Bisimilarity.CCS.Examples.Classical
-- Up-to techniques for strong bisimilarity.
import Bisimilarity.Up-to
import Bisimilarity.Up-to.CCS
import Bisimilarity.Up-to.Counterexamples
-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity.
import Bisimilarity.6-2-5
------------------------------------------------------------------------
-- Expansion
-- A coinductive definition of the expansion ordering.
import Expansion
import Expansion.Equational-reasoning-instances
-- Lemmas related to expansion and CCS.
import Expansion.CCS
-- Some results related to expansion for the delay monad.
import Expansion.Delay-monad
------------------------------------------------------------------------
-- Weak bisimilarity
-- A coinductive definition of weak bisimilarity.
import Bisimilarity.Weak
import Bisimilarity.Weak.Equational-reasoning-instances
-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity.
import Bisimilarity.Weak.Alternative
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances
-- An alternative (non-standard) classical definition of weak
-- bisimilarity.
import Bisimilarity.Weak.Alternative.Classical
-- A comparison of the two alternative definitions of weak
-- bisimilarity.
import Bisimilarity.Weak.Alternative.Comparison
-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent.
import Bisimilarity.Weak.Equivalent
-- Lemmas related to weak bisimilarity and CCS.
import Bisimilarity.Weak.CCS
-- Examples/exercises related to CCS from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.
import Bisimilarity.Weak.CCS.Examples
-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad.
import Bisimilarity.Weak.Delay-monad
-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity.
import Bisimilarity.Weak.Up-to
import Bisimilarity.Weak.Up-to.CCS
-- Up-to techniques for the delay monad and the alternative
-- coinductive definition of weak bisimilarity.
import Bisimilarity.Weak.Alternative.Up-to.Delay-monad
------------------------------------------------------------------------
-- Similarity, continued
-- A coinductive definition of (strong) similarity.
import Similarity
import Similarity.Equational-reasoning-instances
-- Lemmas related to strong similarity for CCS.
import Similarity.CCS
-- A coinductive definition of weak similarity.
import Similarity.Weak
import Similarity.Weak.Equational-reasoning-instances
-- An up-to technique for weak similarity.
import Similarity.Weak.Up-to