![[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 | - | ||
| Agda.Builtin.Unit.html | 2025-05-02 13:13 | 1.7K | |
| Relation.Binary.Latt..> | 2025-05-02 13:13 | 1.7K | |
| Function.Metric.Nat...> | 2025-05-02 13:13 | 1.8K | |
| Agda.css | 2025-05-02 13:13 | 1.8K | |
| Data.Unit.Polymorphi..> | 2025-05-02 13:13 | 1.9K | |
| Data.Unit.Base.html | 2025-05-02 13:13 | 1.9K | |
| Algebra.html | 2025-05-02 13:13 | 1.9K | |
| Agda.Builtin.Word.html | 2025-05-02 13:13 | 2.0K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 2.1K | |
| Relation.Binary.html | 2025-05-02 13:13 | 2.1K | |
| Agda.Builtin.Maybe.html | 2025-05-02 13:13 | 2.3K | |
| Agda.Builtin.IO.html | 2025-05-02 13:13 | 2.4K | |
| Data.Nat.Solver.html | 2025-05-02 13:13 | 2.4K | |
| Agda.Builtin.Equalit..> | 2025-05-02 13:13 | 2.6K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 2.8K | |
| Function.Metric.Core..> | 2025-05-02 13:13 | 2.8K | |
| Function.Metric.Nat...> | 2025-05-02 13:13 | 2.8K | |
| Prelude.Size.html | 2025-05-02 13:13 | 3.1K | |
| Agda.Builtin.Bool.html | 2025-05-02 13:13 | 3.1K | |
| Relation.Nullary.Ind..> | 2025-05-02 13:13 | 3.2K | |
| Agda.Builtin.Cubical..> | 2025-05-02 13:13 | 3.2K | |
| Algebra.Core.html | 2025-05-02 13:13 | 3.3K | |
| Agda.Builtin.Sigma.html | 2025-05-02 13:13 | 3.4K | |
| Agda.Builtin.Int.html | 2025-05-02 13:13 | 3.4K | |
| Equivalence.Erased.C..> | 2025-05-02 13:13 | 3.4K | |
| Data.Unit.Polymorphi..> | 2025-05-02 13:13 | 3.6K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 3.7K | |
| Effect.Empty.html | 2025-05-02 13:13 | 3.8K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 3.8K | |
| Equivalence.Erased.C..> | 2025-05-02 13:13 | 3.9K | |
| Agda.Builtin.Char.html | 2025-05-02 13:13 | 4.0K | |
| Agda.Builtin.Size.html | 2025-05-02 13:13 | 4.2K | |
| Squash.Cubical.html | 2025-05-02 13:13 | 4.4K | |
| Effect.Choice.html | 2025-05-02 13:13 | 4.4K | |
| Data.Empty.Polymorph..> | 2025-05-02 13:13 | 4.5K | |
| Algebra.Solver.Ring...> | 2025-05-02 13:13 | 4.6K | |
| Erased.Without-box-c..> | 2025-05-02 13:13 | 4.6K | |
| Agda.Builtin.List.html | 2025-05-02 13:13 | 4.7K | |
| Data.Fin.Patterns.html | 2025-05-02 13:13 | 4.7K | |
| Algebra.Lattice.Cons..> | 2025-05-02 13:13 | 4.8K | |
| Agda.Builtin.Strict...> | 2025-05-02 13:13 | 4.8K | |
| Data.Empty.html | 2025-05-02 13:13 | 5.0K | |
| Function.Core.html | 2025-05-02 13:13 | 5.0K | |
| Agda.Builtin.Cubical..> | 2025-05-02 13:13 | 5.1K | |
| Data.Product.Relatio..> | 2025-05-02 13:13 | 5.4K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 5.4K | |
| Agda.Primitive.html | 2025-05-02 13:13 | 5.4K | |
| Equality.Path.Isomor..> | 2025-05-02 13:13 | 5.5K | |
| Level.html | 2025-05-02 13:13 | 5.6K | |
| Algebra.Lattice.Prop..> | 2025-05-02 13:13 | 6.2K | |
| Erased.html | 2025-05-02 13:13 | 6.2K | |
| Relation.Nullary.html | 2025-05-02 13:13 | 6.3K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 6.3K | |
| Relation.Binary.Morp..> | 2025-05-02 13:13 | 6.3K | |
| Algebra.Properties.R..> | 2025-05-02 13:13 | 6.4K | |
| Algebra.Lattice.Cons..> | 2025-05-02 13:13 | 6.5K | |
| Excluded-middle.html | 2025-05-02 13:13 | 6.6K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 6.9K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 7.0K | |
| Erased.Box-cong-axio..> | 2025-05-02 13:13 | 7.0K | |
| Data.Bool.ListAction..> | 2025-05-02 13:13 | 7.3K | |
| Algebra.Lattice.Bund..> | 2025-05-02 13:13 | 7.4K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 7.5K | |
| String.html | 2025-05-02 13:13 | 8.1K | |
| Algebra.Properties.S..> | 2025-05-02 13:13 | 8.2K | |
| Function.Indexed.Rel..> | 2025-05-02 13:13 | 8.2K | |
| Container.Tree-sort...> | 2025-05-02 13:13 | 8.9K | |
| Data.Sign.Base.html | 2025-05-02 13:13 | 8.9K | |
| Squash.Erased-matche..> | 2025-05-02 13:13 | 9.2K | |
| Data.List.Membership..> | 2025-05-02 13:13 | 9.3K | |
| Function.Dependent.B..> | 2025-05-02 13:13 | 9.3K | |
| Algebra.Consequences..> | 2025-05-02 13:13 | 9.5K | |
| Queue.Simple.Instanc..> | 2025-05-02 13:13 | 9.5K | |
| Queue.Bankers.Instan..> | 2025-05-02 13:13 | 9.6K | |
| Agda.Builtin.Cubical..> | 2025-05-02 13:13 | 9.7K | |
| IO-monad.html | 2025-05-02 13:13 | 10K | |
| Agda.Builtin.String...> | 2025-05-02 13:13 | 10K | |
| Equality.Proposition..> | 2025-05-02 13:13 | 10K | |
| Relation.Binary.Stru..> | 2025-05-02 13:13 | 10K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 11K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 11K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 11K | |
| Algebra.Morphism.Def..> | 2025-05-02 13:13 | 11K | |
| Algebra.Definitions...> | 2025-05-02 13:13 | 11K | |
| Algebra.Lattice.Prop..> | 2025-05-02 13:13 | 11K | |
| Tree-sort.Examples.html | 2025-05-02 13:13 | 11K | |
| Function.Consequence..> | 2025-05-02 13:13 | 12K | |
| Data.Irrelevant.html | 2025-05-02 13:13 | 12K | |
| Modality.html | 2025-05-02 13:13 | 12K | |
| Relation.Binary.Bund..> | 2025-05-02 13:13 | 12K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 12K | |
| Dec.html | 2025-05-02 13:13 | 12K | |
| Data.Vec.html | 2025-05-02 13:13 | 12K | |
| Data.Sum.html | 2025-05-02 13:13 | 12K | |
| Relation.Binary.Latt..> | 2025-05-02 13:13 | 13K | |
| Data.Bool.Base.html | 2025-05-02 13:13 | 13K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 13K | |
| Sum.html | 2025-05-02 13:13 | 13K | |
| Algebra.Properties.A..> | 2025-05-02 13:13 | 13K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 13K | |
| Effect.Functor.html | 2025-05-02 13:13 | 13K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 14K | |
| Induction.html | 2025-05-02 13:13 | 14K | |
| Erased.Basics.html | 2025-05-02 13:13 | 14K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 14K | |
| Data.Nat.Divisibilit..> | 2025-05-02 13:13 | 16K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 16K | |
| Algebra.Properties.Q..> | 2025-05-02 13:13 | 17K | |
| Relation.Binary.Inde..> | 2025-05-02 13:13 | 17K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 17K | |
| Modality.Identity.html | 2025-05-02 13:13 | 17K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 18K | |
| Injection.html | 2025-05-02 13:13 | 18K | |
| Function.Metric.Nat...> | 2025-05-02 13:13 | 18K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 18K | |
| Accessibility.Erased..> | 2025-05-02 13:13 | 18K | |
| Monad.Raw.html | 2025-05-02 13:13 | 18K | |
| Function.Metric.Nat...> | 2025-05-02 13:13 | 19K | |
| Algebra.Lattice.Cons..> | 2025-05-02 13:13 | 19K | |
| Data.Parity.Base.html | 2025-05-02 13:13 | 19K | |
| Equality.Proposition..> | 2025-05-02 13:13 | 19K | |
| Algebra.Definitions...> | 2025-05-02 13:13 | 19K | |
| Function.Properties...> | 2025-05-02 13:13 | 19K | |
| Relation.Binary.Core..> | 2025-05-02 13:13 | 19K | |
| Tactic.By.Parametris..> | 2025-05-02 13:13 | 20K | |
| Data.List.Membership..> | 2025-05-02 13:13 | 20K | |
| Relation.Nullary.Rec..> | 2025-05-02 13:13 | 20K | |
| Relation.Nullary.Neg..> | 2025-05-02 13:13 | 21K | |
| Algebra.Properties.L..> | 2025-05-02 13:13 | 21K | |
| Function.Properties...> | 2025-05-02 13:13 | 21K | |
| Algebra.Definitions...> | 2025-05-02 13:13 | 21K | |
| Axiom.Extensionality..> | 2025-05-02 13:13 | 21K | |
| Axiom.UniquenessOfId..> | 2025-05-02 13:13 | 21K | |
| Function.Definitions..> | 2025-05-02 13:13 | 21K | |
| Function.Metric.Stru..> | 2025-05-02 13:13 | 22K | |
| Function.Consequence..> | 2025-05-02 13:13 | 23K | |
| Function.Properties...> | 2025-05-02 13:13 | 23K | |
| Agda.Builtin.Nat.html | 2025-05-02 13:13 | 23K | |
| Agda.Primitive.Cubic..> | 2025-05-02 13:13 | 24K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 24K | |
| Data.Nat.Induction.html | 2025-05-02 13:13 | 25K | |
| Data.Sum.Base.html | 2025-05-02 13:13 | 26K | |
| Data.Unit.Polymorphi..> | 2025-05-02 13:13 | 27K | |
| Monad.Reader.html | 2025-05-02 13:13 | 27K | |
| Function-universe.Si..> | 2025-05-02 13:13 | 28K | |
| Function.Metric.Nat...> | 2025-05-02 13:13 | 29K | |
| Const.html | 2025-05-02 13:13 | 31K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 31K | |
| Algebra.Properties.M..> | 2025-05-02 13:13 | 32K | |
| Pointed-type.Connect..> | 2025-05-02 13:13 | 32K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 32K | |
| Agda.Builtin.Float.html | 2025-05-02 13:13 | 32K | |
| Data.Maybe.Relation...> | 2025-05-02 13:13 | 33K | |
| Data.Sum.Algebra.html | 2025-05-02 13:13 | 33K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 34K | |
| Interval.html | 2025-05-02 13:13 | 34K | |
| Function.Consequence..> | 2025-05-02 13:13 | 35K | |
| Effect.Monad.html | 2025-05-02 13:13 | 35K | |
| Function.Metric.Defi..> | 2025-05-02 13:13 | 35K | |
| Vec.html | 2025-05-02 13:13 | 36K | |
| Effect.Applicative.html | 2025-05-02 13:13 | 36K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 36K | |
| Data.These.Base.html | 2025-05-02 13:13 | 37K | |
| Monad.State.html | 2025-05-02 13:13 | 37K | |
| Function.Metric.Bund..> | 2025-05-02 13:13 | 37K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 37K | |
| Data.Maybe.Base.html | 2025-05-02 13:13 | 37K | |
| Relation.Binary.Refl..> | 2025-05-02 13:13 | 37K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 37K | |
| Relation.Nullary.Neg..> | 2025-05-02 13:13 | 38K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 38K | |
| Relation.Binary.Morp..> | 2025-05-02 13:13 | 38K | |
| Relation.Nullary.Dec..> | 2025-05-02 13:13 | 39K | |
| Algebra.Properties.S..> | 2025-05-02 13:13 | 39K | |
| Tree-sort.Partial.html | 2025-05-02 13:13 | 39K | |
| Vec.Data.html | 2025-05-02 13:13 | 39K | |
| Algebra.Lattice.Stru..> | 2025-05-02 13:13 | 40K | |
| Integer.Basics.html | 2025-05-02 13:13 | 40K | |
| Erased.With-K.html | 2025-05-02 13:13 | 41K | |
| Relation.Nullary.Ref..> | 2025-05-02 13:13 | 42K | |
| Algebra.Lattice.Prop..> | 2025-05-02 13:13 | 43K | |
| Algebra.Properties.R..> | 2025-05-02 13:13 | 44K | |
| Data.List.Membership..> | 2025-05-02 13:13 | 44K | |
| Relation.Unary.Predi..> | 2025-05-02 13:13 | 44K | |
| Algebra.Solver.Ring...> | 2025-05-02 13:13 | 45K | |
| Data.Sum.Function.Pr..> | 2025-05-02 13:13 | 46K | |
| Function.Properties...> | 2025-05-02 13:13 | 46K | |
| Function.Construct.I..> | 2025-05-02 13:13 | 46K | |
| Squash.Irrelevance.html | 2025-05-02 13:13 | 47K | |
| Vec.Dependent.html | 2025-05-02 13:13 | 47K | |
| Function.Structures...> | 2025-05-02 13:13 | 47K | |
| Algebra.Morphism.html | 2025-05-02 13:13 | 47K | |
| Vec.Function.html | 2025-05-02 13:13 | 47K | |
| Algebra.Consequences..> | 2025-05-02 13:13 | 48K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 49K | |
| Data.Product.Functio..> | 2025-05-02 13:13 | 49K | |
| Queue.Truncated.Inst..> | 2025-05-02 13:13 | 49K | |
| Erased.Cubical.html | 2025-05-02 13:13 | 49K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 50K | |
| Logical-equivalence...> | 2025-05-02 13:13 | 50K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 51K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 51K | |
| Maybe.html | 2025-05-02 13:13 | 52K | |
| Agda.Builtin.Cubical..> | 2025-05-02 13:13 | 53K | |
| Algebra.Lattice.Bund..> | 2025-05-02 13:13 | 53K | |
| H-level.html | 2025-05-02 13:13 | 53K | |
| Agda.Builtin.Cubical..> | 2025-05-02 13:13 | 53K | |
| Function.Properties...> | 2025-05-02 13:13 | 53K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 54K | |
| Data.Product.Algebra..> | 2025-05-02 13:13 | 55K | |
| Omniscience.html | 2025-05-02 13:13 | 55K | |
| Container.Stream.html | 2025-05-02 13:13 | 55K | |
| Data.Maybe.Relation...> | 2025-05-02 13:13 | 56K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 56K | |
| Data.Product.Propert..> | 2025-05-02 13:13 | 57K | |
| Nat.Wrapper.Cubical...> | 2025-05-02 13:13 | 58K | |
| Finite-subset.Kurato..> | 2025-05-02 13:13 | 59K | |
| Modality.Box-cong.html | 2025-05-02 13:13 | 59K | |
| Nat.Solver.html | 2025-05-02 13:13 | 59K | |
| Preimage.html | 2025-05-02 13:13 | 59K | |
| Tactic.By.Parametris..> | 2025-05-02 13:13 | 59K | |
| Data.Product.Functio..> | 2025-05-02 13:13 | 59K | |
| Data.Sum.Properties...> | 2025-05-02 13:13 | 60K | |
| Queue.Simple.html | 2025-05-02 13:13 | 61K | |
| Queue.Quotiented.Ins..> | 2025-05-02 13:13 | 61K | |
| Container.Tree-sort...> | 2025-05-02 13:13 | 62K | |
| Data.List.Extrema.Co..> | 2025-05-02 13:13 | 62K | |
| Relation.Binary.Latt..> | 2025-05-02 13:13 | 63K | |
| Tree.html | 2025-05-02 13:13 | 64K | |
| Nat.Wrapper.Cubical...> | 2025-05-02 13:13 | 65K | |
| Adjunction.html | 2025-05-02 13:13 | 65K | |
| Algebra.Structures.B..> | 2025-05-02 13:13 | 65K | |
| Algebra.Bundles.Raw...> | 2025-05-02 13:13 | 66K | |
| Equality.Path.Unival..> | 2025-05-02 13:13 | 66K | |
| Data.Vec.Functional...> | 2025-05-02 13:13 | 67K | |
| Embedding.Erased.html | 2025-05-02 13:13 | 67K | |
| Data.Vec.Bounded.Bas..> | 2025-05-02 13:13 | 68K | |
| Data.Nat.Generalised..> | 2025-05-02 13:13 | 68K | |
| Sphere.html | 2025-05-02 13:13 | 68K | |
| Relation.Binary.Stru..> | 2025-05-02 13:13 | 68K | |
| Relation.Binary.Latt..> | 2025-05-02 13:13 | 69K | |
| Relation.Nullary.Dec..> | 2025-05-02 13:13 | 69K | |
| Algebra.Properties.G..> | 2025-05-02 13:13 | 70K | |
| Equivalence.Erased.C..> | 2025-05-02 13:13 | 71K | |
| Function.Construct.S..> | 2025-05-02 13:13 | 72K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 73K | |
| Container.Indexed.Va..> | 2025-05-02 13:13 | 73K | |
| Data.Sum.Function.Se..> | 2025-05-02 13:13 | 73K | |
| Nat.Eliminator.html | 2025-05-02 13:13 | 74K | |
| Bool.html | 2025-05-02 13:13 | 74K | |
| Pointed-type.Homotop..> | 2025-05-02 13:13 | 74K | |
| Equality.Decidable-U..> | 2025-05-02 13:13 | 76K | |
| Torus.html | 2025-05-02 13:13 | 76K | |
| Function.Base.html | 2025-05-02 13:13 | 76K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 77K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 80K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 82K | |
| Equivalence-relation..> | 2025-05-02 13:13 | 82K | |
| Algebra.Construct.Li..> | 2025-05-02 13:13 | 84K | |
| Bool.Very-stable.html | 2025-05-02 13:13 | 86K | |
| Quotient.Erased.Basi..> | 2025-05-02 13:13 | 87K | |
| Data.Product.Base.html | 2025-05-02 13:13 | 87K | |
| Surjection.html | 2025-05-02 13:13 | 88K | |
| Queue.html | 2025-05-02 13:13 | 88K | |
| Relation.Binary.Reas..> | 2025-05-02 13:13 | 90K | |
| Queue.Bankers.html | 2025-05-02 13:13 | 91K | |
| Data.Vec.N-ary.html | 2025-05-02 13:13 | 92K | |
| Embedding.html | 2025-05-02 13:13 | 93K | |
| Container.Tree.html | 2025-05-02 13:13 | 93K | |
| Relation.Unary.html | 2025-05-02 13:13 | 93K | |
| Modality.Zero.html | 2025-05-02 13:13 | 94K | |
| Accessibility.html | 2025-05-02 13:13 | 94K | |
| Induction.WellFounde..> | 2025-05-02 13:13 | 96K | |
| Algebra.Solver.Ring...> | 2025-05-02 13:13 | 96K | |
| Double-negation.html | 2025-05-02 13:13 | 96K | |
| Queue.Quotiented.html | 2025-05-02 13:13 | 96K | |
| Equality.Decision-pr..> | 2025-05-02 13:13 | 97K | |
| Data.Product.Relatio..> | 2025-05-02 13:13 | 97K | |
| Equivalence.Erased.B..> | 2025-05-02 13:13 | 97K | |
| Relation.Binary.Bund..> | 2025-05-02 13:13 | 98K | |
| Relation.Binary.Defi..> | 2025-05-02 13:13 | 98K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 99K | |
| Equality.Groupoid.html | 2025-05-02 13:13 | 100K | |
| Relation.Binary.Cons..> | 2025-05-02 13:13 | 101K | |
| Pullback.html | 2025-05-02 13:13 | 102K | |
| Data.Nat.Base.html | 2025-05-02 13:13 | 103K | |
| Colimit.Sequential.E..> | 2025-05-02 13:13 | 105K | |
| Data.Sum.Relation.Bi..> | 2025-05-02 13:13 | 106K | |
| Pushout.html | 2025-05-02 13:13 | 107K | |
| Tree-sort.Full.html | 2025-05-02 13:13 | 107K | |
| Records-with-with.html | 2025-05-02 13:13 | 108K | |
| Algebra.Construct.Na..> | 2025-05-02 13:13 | 109K | |
| Relation.Binary.Prop..> | 2025-05-02 13:13 | 110K | |
| Algebra.Properties.C..> | 2025-05-02 13:13 | 112K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 112K | |
| Data.Fin.Base.html | 2025-05-02 13:13 | 114K | |
| Monad.html | 2025-05-02 13:13 | 115K | |
| Structure-identity-p..> | 2025-05-02 13:13 | 116K | |
| Algebra.Definitions...> | 2025-05-02 13:13 | 118K | |
| Function.Construct.C..> | 2025-05-02 13:13 | 119K | |
| Equality.Instances-r..> | 2025-05-02 13:13 | 120K | |
| Function.Related.Pro..> | 2025-05-02 13:13 | 120K | |
| Tactic.By.Propositio..> | 2025-05-02 13:13 | 121K | |
| M.html | 2025-05-02 13:13 | 122K | |
| Relation.Unary.Prope..> | 2025-05-02 13:13 | 123K | |
| Prelude.html | 2025-05-02 13:13 | 123K | |
| Tactic.By.Path.html | 2025-05-02 13:13 | 125K | |
| Bi-invertibility.html | 2025-05-02 13:13 | 126K | |
| Equivalence.Contract..> | 2025-05-02 13:13 | 128K | |
| Function.Bundles.html | 2025-05-02 13:13 | 128K | |
| Equality.Tactic.html | 2025-05-02 13:13 | 129K | |
| Data.List.Extrema.html | 2025-05-02 13:13 | 132K | |
| Bi-invertibility.Era..> | 2025-05-02 13:13 | 132K | |
| Data.List.Relation.B..> | 2025-05-02 13:13 | 132K | |
| Equivalence.Half-adj..> | 2025-05-02 13:13 | 133K | |
| Tactic.By.html | 2025-05-02 13:13 | 145K | |
| Container.Indexed.html | 2025-05-02 13:13 | 146K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 146K | |
| Data.List.Effectful...> | 2025-05-02 13:13 | 147K | |
| Modality.Empty-modal..> | 2025-05-02 13:13 | 150K | |
| Data.Vec.Base.html | 2025-05-02 13:13 | 150K | |
| Suspension.html | 2025-05-02 13:13 | 152K | |
| Equivalence.Erased.C..> | 2025-05-02 13:13 | 155K | |
| Figure-of-eight.html | 2025-05-02 13:13 | 155K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 157K | |
| Tactic.Sigma-cong.html | 2025-05-02 13:13 | 159K | |
| Colimit.Sequential.html | 2025-05-02 13:13 | 163K | |
| Queue.Truncated.html | 2025-05-02 13:13 | 163K | |
| Data.Product.Functio..> | 2025-05-02 13:13 | 163K | |
| Agda.Builtin.Reflect..> | 2025-05-02 13:13 | 164K | |
| Function.Related.Typ..> | 2025-05-02 13:13 | 165K | |
| Container.List.html | 2025-05-02 13:13 | 168K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 168K | |
| Data.Nat.Divisibilit..> | 2025-05-02 13:13 | 170K | |
| TC-monad.html | 2025-05-02 13:13 | 170K | |
| Erased.Erased-matche..> | 2025-05-02 13:13 | 172K | |
| Container.Indexed.Va..> | 2025-05-02 13:13 | 176K | |
| Colimit.Sequential.V..> | 2025-05-02 13:13 | 179K | |
| Algebra.Consequences..> | 2025-05-02 13:13 | 179K | |
| Fin.html | 2025-05-02 13:13 | 183K | |
| Integer.html | 2025-05-02 13:13 | 183K | |
| Circle.Erased.html | 2025-05-02 13:13 | 184K | |
| Modality.Erased-matc..> | 2025-05-02 13:13 | 186K | |
| Groupoid.html | 2025-05-02 13:13 | 189K | |
| Extensionality.html | 2025-05-02 13:13 | 189K | |
| Modality.Commutes-wi..> | 2025-05-02 13:13 | 189K | |
| Localisation.html | 2025-05-02 13:13 | 196K | |
| Pointed-type.html | 2025-05-02 13:13 | 198K | |
| Nat.Wrapper.html | 2025-05-02 13:13 | 205K | |
| Container.Indexed.Co..> | 2025-05-02 13:13 | 206K | |
| Data.Bool.Properties..> | 2025-05-02 13:13 | 207K | |
| Algebra.Morphism.Str..> | 2025-05-02 13:13 | 210K | |
| Group.html | 2025-05-02 13:13 | 214K | |
| List.All.html | 2025-05-02 13:13 | 221K | |
| Data.List.Base.html | 2025-05-02 13:13 | 223K | |
| Group.Cyclic.html | 2025-05-02 13:13 | 223K | |
| Data.Nat.DivMod.Core..> | 2025-05-02 13:13 | 224K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 225K | |
| Container.Indexed.M...> | 2025-05-02 13:13 | 226K | |
| Bijection.html | 2025-05-02 13:13 | 226K | |
| Algebra.Structures.html | 2025-05-02 13:13 | 233K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 235K | |
| Modality.Left-exact...> | 2025-05-02 13:13 | 238K | |
| Data.List.Membership..> | 2025-05-02 13:13 | 239K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 246K | |
| Modality.Very-modal...> | 2025-05-02 13:13 | 251K | |
| Squash.html | 2025-05-02 13:13 | 251K | |
| Coherently-constant...> | 2025-05-02 13:13 | 257K | |
| Equality.Path.Isomor..> | 2025-05-02 13:13 | 259K | |
| Data.List.Membership..> | 2025-05-02 13:13 | 261K | |
| Container.Indexed.Va..> | 2025-05-02 13:13 | 263K | |
| Finite-subset.Kurato..> | 2025-05-02 13:13 | 264K | |
| List.html | 2025-05-02 13:13 | 265K | |
| Join.html | 2025-05-02 13:13 | 266K | |
| Quotient.Erased.html | 2025-05-02 13:13 | 268K | |
| Finite-subset.Listed..> | 2025-05-02 13:13 | 270K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 277K | |
| Algebra.Bundles.html | 2025-05-02 13:13 | 282K | |
| H-level.Truncation.html | 2025-05-02 13:13 | 286K | |
| Algebra.Solver.Ring...> | 2025-05-02 13:13 | 288K | |
| Algebra.Lattice.Prop..> | 2025-05-02 13:13 | 292K | |
| Container.html | 2025-05-02 13:13 | 296K | |
| Nat.Binary.html | 2025-05-02 13:13 | 305K | |
| List.All.Recursive.html | 2025-05-02 13:13 | 315K | |
| Eilenberg-MacLane-sp..> | 2025-05-02 13:13 | 318K | |
| Nullification.Modali..> | 2025-05-02 13:13 | 324K | |
| Functor.html | 2025-05-02 13:13 | 332K | |
| Erased.Level-2.html | 2025-05-02 13:13 | 334K | |
| For-iterated-equalit..> | 2025-05-02 13:13 | 337K | |
| Finite-subset.Listed..> | 2025-05-02 13:13 | 338K | |
| Integer.Quotient.html | 2025-05-02 13:13 | 344K | |
| Equality.Path.html | 2025-05-02 13:13 | 347K | |
| Circle.html | 2025-05-02 13:13 | 352K | |
| Equivalence.List.html | 2025-05-02 13:13 | 355K | |
| Data.Nat.DivMod.html | 2025-05-02 13:13 | 356K | |
| Container.Indexed.Al..> | 2025-05-02 13:13 | 366K | |
| Colist.html | 2025-05-02 13:13 | 375K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 388K | |
| H-level.Closure.html | 2025-05-02 13:13 | 406K | |
| Equivalence.Path-spl..> | 2025-05-02 13:13 | 413K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 417K | |
| Container.Indexed.Va..> | 2025-05-02 13:13 | 420K | |
| Finite-subset.Listed..> | 2025-05-02 13:13 | 425K | |
| Quotient.html | 2025-05-02 13:13 | 425K | |
| Conat.html | 2025-05-02 13:13 | 432K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 447K | |
| Data.List.Relation.U..> | 2025-05-02 13:13 | 459K | |
| Nat.html | 2025-05-02 13:13 | 476K | |
| Quotient.Families-of..> | 2025-05-02 13:13 | 484K | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 489K | |
| Equivalence.html | 2025-05-02 13:13 | 502K | |
| Data.Fin.Properties...> | 2025-05-02 13:13 | 547K | |
| Quotient.Higher-cons..> | 2025-05-02 13:13 | 551K | |
| H-level.Truncation.P..> | 2025-05-02 13:13 | 558K | |
| H-level.Truncation.C..> | 2025-05-02 13:13 | 584K | |
| Container.Indexed.M...> | 2025-05-02 13:13 | 594K | |
| Quotient.Set-truncat..> | 2025-05-02 13:13 | 598K | |
| Bag-equivalence.html | 2025-05-02 13:13 | 648K | |
| Finite-subset.Listed..> | 2025-05-02 13:13 | 650K | |
| Nullification.html | 2025-05-02 13:13 | 665K | |
| Univalence-axiom.html | 2025-05-02 13:13 | 706K | |
| Category.html | 2025-05-02 13:13 | 799K | |
| Modality.Has-choice...> | 2025-05-02 13:13 | 861K | |
| Data.List.Properties..> | 2025-05-02 13:13 | 867K | |
| Equivalence.Erased.html | 2025-05-02 13:13 | 880K | |
| Finite-subset.Listed..> | 2025-05-02 13:13 | 932K | |
| Data.Nat.Properties...> | 2025-05-02 13:13 | 938K | |
| Equality.html | 2025-05-02 13:13 | 1.0M | |
| Erased.Stability.html | 2025-05-02 13:13 | 1.1M | |
| Abstract-binding-tre..> | 2025-05-02 13:13 | 1.2M | |
| Erased.Level-1.html | 2025-05-02 13:13 | 1.2M | |
| Univalence-axiom.Iso..> | 2025-05-02 13:13 | 1.2M | |
| Structure-identity-p..> | 2025-05-02 13:13 | 1.2M | |
| Modality.Basics.html | 2025-05-02 13:13 | 2.1M | |
| Function-universe.html | 2025-05-02 13:13 | 2.6M | |
------------------------------------------------------------------------
-- Experiments related to equality
--
-- Nils Anders Danielsson
--
-- Some files have been developed in collaboration with others, see
-- the individual files.
------------------------------------------------------------------------
{-# OPTIONS --cubical --with-K --guardedness --sized-types --prop #-}
module README where
-- "Safe" code that uses --cubical-compatible.
import README.Safe.Cubical-compatible
-- "Safe" code that uses --cubical-compatible and --erased-matches.
import README.Safe.Cubical-compatible.Erased-matches
-- "Safe" code that uses --cubical-compatible and --prop.
import README.Safe.Cubical-compatible.Prop
-- "Safe" code that uses --cubical-compatible, --prop and
-- --erased-matches.
import README.Safe.Cubical-compatible.Prop.Erased-matches
-- "Safe" code that uses --erased-cubical.
import README.Safe.Cubical.Erased
-- "Safe" code that uses --erased-cubical and --guardedness.
import README.Safe.Cubical.Erased.Guardedness
-- "Safe" code that uses --erased-cubical and --prop.
import README.Safe.Cubical.Erased.Prop
-- "Safe" code that uses --cubical.
import README.Safe.Cubical
-- "Safe" code that uses --with-K.
import README.Safe.With-K
-- Code which might depend on potentially unsafe features (other than
-- --sized-types).
import README.Unsafe
-- Code which is "safe", except for the use of --sized-types.
import README.Unsafe.Sized-types
-- Code related to the paper "Logical properties of a modality for
-- erasure". This code uses both --cubical and --with-K, but not at
-- the same time, except in the module README.Erased, which for that
-- reason cannot use --safe.
import README.Erased