Index of /~nad/listings/equality

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]Agda.Builtin.Bool.html 2023-09-29 17:39 3.1K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:39 2.6K 
[TXT]Agda.Primitive.html 2023-09-29 17:39 5.4K 
[TXT]Agda.css 2023-09-29 17:39 1.8K 
[TXT]Agda.Builtin.Char.html 2023-09-29 17:39 4.0K 
[TXT]Agda.Builtin.List.html 2023-09-29 17:39 4.7K 
[TXT]Agda.Builtin.Maybe.html2023-09-29 17:39 2.3K 
[TXT]Agda.Builtin.Nat.html 2023-09-29 17:39 23K 
[TXT]Agda.Builtin.Sigma.html2023-09-29 17:39 3.4K 
[TXT]Agda.Builtin.Unit.html 2023-09-29 17:39 1.7K 
[TXT]Agda.Builtin.String...>2023-09-29 17:39 10K 
[TXT]Logical-equivalence...>2023-09-29 17:39 50K 
[TXT]Prelude.html 2023-09-29 17:39 123K 
[TXT]Equality.html 2023-09-29 17:39 1.0M 
[TXT]Surjection.html 2023-09-29 17:39 88K 
[TXT]Nat.html 2023-09-29 17:39 476K 
[TXT]H-level.html 2023-09-29 17:39 53K 
[TXT]Equality.Decidable-U..>2023-09-29 17:39 76K 
[TXT]Equality.Decision-pr..>2023-09-29 17:39 97K 
[TXT]Injection.html 2023-09-29 17:39 18K 
[TXT]Bijection.html 2023-09-29 17:39 226K 
[TXT]Preimage.html 2023-09-29 17:39 59K 
[TXT]Equivalence.Contract..>2023-09-29 17:39 128K 
[TXT]Equivalence.Half-adj..>2023-09-29 17:39 133K 
[TXT]Extensionality.html 2023-09-29 17:39 189K 
[TXT]Agda.Builtin.Int.html 2023-09-29 17:39 3.4K 
[TXT]Excluded-middle.html 2023-09-29 17:39 6.6K 
[TXT]H-level.Closure.html 2023-09-29 17:39 406K 
[TXT]Integer.Basics.html 2023-09-29 17:39 40K 
[TXT]Groupoid.html 2023-09-29 17:39 189K 
[TXT]Equivalence.html 2023-09-29 17:39 502K 
[TXT]Embedding.html 2023-09-29 17:39 82K 
[TXT]Equality.Proposition..>2023-09-29 17:39 19K 
[TXT]Erased.Basics.html 2023-09-29 17:39 14K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:39 70K 
[TXT]Equivalence.Erased.B..>2023-09-29 17:39 97K 
[TXT]Function-universe.html 2023-09-29 17:39 2.5M 
[TXT]Accessibility.html 2023-09-29 17:39 94K 
[TXT]Monad.Raw.html 2023-09-29 17:39 18K 
[TXT]Monad.html 2023-09-29 17:39 115K 
[TXT]Bool.html 2023-09-29 17:39 74K 
[TXT]Erased.Box-cong-axio..>2023-09-29 17:39 7.0K 
[TXT]Univalence-axiom.html 2023-09-29 17:39 706K 
[TXT]Equivalence-relation..>2023-09-29 17:39 82K 
[TXT]Level.html 2023-09-29 17:39 5.6K 
[TXT]Function.Base.html 2023-09-29 17:39 75K 
[TXT]Data.Bool.Base.html 2023-09-29 17:39 13K 
[TXT]Data.Empty.html 2023-09-29 17:39 4.1K 
[TXT]Data.Irrelevant.html 2023-09-29 17:39 12K 
[TXT]Data.Unit.Base.html 2023-09-29 17:39 1.9K 
[TXT]Data.Empty.Irrelevan..>2023-09-29 17:39 2.2K 
[TXT]Data.Sum.Base.html 2023-09-29 17:39 26K 
[TXT]Data.Product.Base.html 2023-09-29 17:39 87K 
[TXT]Data.These.Base.html 2023-09-29 17:39 36K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:39 21K 
[TXT]Relation.Nullary.Ref..>2023-09-29 17:39 34K 
[TXT]Data.Maybe.Base.html 2023-09-29 17:39 37K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:39 56K 
[TXT]Relation.Binary.Core..>2023-09-29 17:39 19K 
[TXT]Relation.Binary.Defi..>2023-09-29 17:39 91K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 10K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 45K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 11K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 2.1K 
[TXT]Relation.Nullary.html 2023-09-29 17:39 6.5K 
[TXT]Relation.Unary.html 2023-09-29 17:39 91K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 101K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:39 3.3K 
[TXT]Effect.Choice.html 2023-09-29 17:39 4.4K 
[TXT]Effect.Empty.html 2023-09-29 17:39 3.4K 
[TXT]Effect.Functor.html 2023-09-29 17:39 13K 
[TXT]Relation.Binary.Stru..>2023-09-29 17:39 62K 
[TXT]Effect.Applicative.html2023-09-29 17:39 36K 
[TXT]Effect.Monad.html 2023-09-29 17:39 32K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:39 38K 
[TXT]Algebra.Core.html 2023-09-29 17:39 3.3K 
[TXT]Relation.Binary.Bund..>2023-09-29 17:39 66K 
[TXT]Relation.Binary.html 2023-09-29 17:39 1.9K 
[TXT]Algebra.Definitions...>2023-09-29 17:39 118K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 7.1K 
[TXT]Function.Definitions..>2023-09-29 17:39 21K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 20K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 7.4K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 165K 
[TXT]Algebra.Structures.html2023-09-29 17:39 210K 
[TXT]Algebra.Structures.B..>2023-09-29 17:39 64K 
[TXT]Algebra.Bundles.Raw...>2023-09-29 17:39 54K 
[TXT]Algebra.Bundles.html 2023-09-29 17:39 255K 
[TXT]Algebra.html 2023-09-29 17:39 1.9K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 18K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 15K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 5.5K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 104K 
[TXT]Function.Equality.html 2023-09-29 17:39 40K 
[TXT]Function.Consequence..>2023-09-29 17:39 22K 
[TXT]Function.Consequence..>2023-09-29 17:39 34K 
[TXT]Function.Structures...>2023-09-29 17:39 43K 
[TXT]Function.Bundles.html 2023-09-29 17:39 110K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:39 23K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:39 32K 
[TXT]Axiom.Extensionality..>2023-09-29 17:39 21K 
[TXT]Data.Parity.Base.html 2023-09-29 17:39 19K 
[TXT]Data.Sign.Base.html 2023-09-29 17:39 8.9K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 53K 
[TXT]Data.Nat.Base.html 2023-09-29 17:39 83K 
[TXT]Data.Fin.Base.html 2023-09-29 17:39 117K 
[TXT]Data.List.Base.html 2023-09-29 17:39 194K 
[TXT]Data.Vec.Base.html 2023-09-29 17:39 153K 
[TXT]Data.Vec.N-ary.html 2023-09-29 17:39 92K 
[TXT]Algebra.Properties.G..>2023-09-29 17:39 52K 
[TXT]Relation.Binary.Refl..>2023-09-29 17:39 37K 
[TXT]Algebra.Properties.A..>2023-09-29 17:39 12K 
[TXT]Function.Core.html 2023-09-29 17:39 5.0K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:39 6.3K 
[TXT]Algebra.Morphism.Def..>2023-09-29 17:39 11K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:39 38K 
[TXT]Algebra.Morphism.Str..>2023-09-29 17:39 177K 
[TXT]Algebra.Morphism.html 2023-09-29 17:39 47K 
[TXT]Algebra.Properties.R..>2023-09-29 17:39 41K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:39 43K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 72K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 9.8K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 69K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 34K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 17K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 39K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 17K 
[TXT]Algebra.Lattice.Stru..>2023-09-29 17:39 41K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 45K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 3.5K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 109K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:39 7.2K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:39 51K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 6.3K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 18K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 57K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 4.5K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 18K 
[TXT]Data.Unit.Properties..>2023-09-29 17:39 16K 
[TXT]Data.Unit.html 2023-09-29 17:39 1.7K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 69K 
[TXT]Algebra.Properties.S..>2023-09-29 17:39 8.2K 
[TXT]Algebra.Properties.C..>2023-09-29 17:39 112K 
[TXT]Function.Metric.Core..>2023-09-29 17:39 2.8K 
[TXT]Function.Metric.Defi..>2023-09-29 17:39 35K 
[TXT]Function.Metric.Stru..>2023-09-29 17:39 22K 
[TXT]Function.Metric.Bund..>2023-09-29 17:39 37K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 2.6K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 17K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 28K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 18K 
[TXT]Function.Equivalence..>2023-09-29 17:39 40K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 1.8K 
[TXT]Induction.html 2023-09-29 17:39 17K 
[TXT]Induction.WellFounde..>2023-09-29 17:39 87K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 12K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 61K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 68K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 1.7K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 77K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 11K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 6.0K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 42K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 293K 
[TXT]Data.Bool.Properties..>2023-09-29 17:39 204K 
[TXT]Data.Nat.Properties...>2023-09-29 17:39 908K 
[TXT]Algebra.Definitions...>2023-09-29 17:39 16K 
[TXT]Algebra.Definitions...>2023-09-29 17:39 11K 
[TXT]Data.Vec.Functional...>2023-09-29 17:39 69K 
[TXT]Algebra.Definitions...>2023-09-29 17:39 21K 
[TXT]Algebra.Properties.M..>2023-09-29 17:39 30K 
[TXT]Data.Nat.html 2023-09-29 17:39 5.7K 
[TXT]Algebra.Properties.S..>2023-09-29 17:39 38K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:39 96K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:39 294K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:39 4.3K 
[TXT]Data.Nat.Solver.html 2023-09-29 17:39 2.4K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 38K 
[TXT]Data.List.Membership..>2023-09-29 17:39 19K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 2.8K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 10K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 83K 
[TXT]Algebra.Construct.Li..>2023-09-29 17:39 83K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 7.3K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 13K 
[TXT]Data.List.Extrema.Co..>2023-09-29 17:39 60K 
[TXT]Data.Sum.Properties...>2023-09-29 17:39 60K 
[TXT]Data.Product.Propert..>2023-09-29 17:39 55K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:39 23K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:39 1.9K 
[TXT]Function.Construct.I..>2023-09-29 17:39 45K 
[TXT]Function.Construct.C..>2023-09-29 17:39 115K 
[TXT]Function.Construct.S..>2023-09-29 17:39 72K 
[TXT]Data.Empty.Polymorph..>2023-09-29 17:39 3.8K 
[TXT]Data.Sum.Algebra.html 2023-09-29 17:39 30K 
[TXT]Function.Properties...>2023-09-29 17:39 28K 
[TXT]Data.Product.Algebra..>2023-09-29 17:39 52K 
[TXT]Data.Fin.Patterns.html 2023-09-29 17:39 4.3K 
[TXT]Relation.Unary.Prope..>2023-09-29 17:39 113K 
[TXT]Data.Fin.Properties...>2023-09-29 17:39 540K 
[TXT]Data.Nat.DivMod.Core..>2023-09-29 17:39 222K 
[TXT]Data.Nat.Induction.html2023-09-29 17:39 25K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:39 15K 
[TXT]Data.Nat.DivMod.html 2023-09-29 17:39 363K 
[TXT]Data.List.Membership..>2023-09-29 17:39 9.3K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:39 158K 
[TXT]Data.Product.Relatio..>2023-09-29 17:39 5.4K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 110K 
[TXT]Data.List.Properties..>2023-09-29 17:39 618K 
[TXT]Function.Injection.html2023-09-29 17:39 23K 
[TXT]Function.LeftInverse..>2023-09-29 17:39 42K 
[TXT]Function.Surjection...>2023-09-29 17:39 33K 
[TXT]Function.Bijection.html2023-09-29 17:39 33K 
[TXT]Function.Inverse.html 2023-09-29 17:39 60K 
[TXT]Function.Properties...>2023-09-29 17:39 7.7K 
[TXT]Function.Properties...>2023-09-29 17:39 13K 
[TXT]Function.Properties...>2023-09-29 17:39 20K 
[TXT]Function.Related.Pro..>2023-09-29 17:39 126K 
[TXT]Function.Related.html 2023-09-29 17:39 163K 
[TXT]Data.Product.Relatio..>2023-09-29 17:39 113K 
[TXT]Data.Product.Functio..>2023-09-29 17:39 55K 
[TXT]Function.HalfAdjoint..>2023-09-29 17:39 46K 
[TXT]Relation.Nullary.Ind..>2023-09-29 17:39 3.2K 
[TXT]Data.Product.Functio..>2023-09-29 17:39 36K 
[TXT]Data.Sum.Relation.Bi..>2023-09-29 17:39 111K 
[TXT]Data.Sum.Function.Se..>2023-09-29 17:39 56K 
[TXT]Data.Sum.Function.Pr..>2023-09-29 17:39 34K 
[TXT]Function.Related.Typ..>2023-09-29 17:39 185K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 6.3K 
[TXT]Data.Product.Functio..>2023-09-29 17:39 159K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 78K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 36K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 5.7K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 26K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 37K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 127K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 48K 
[TXT]Data.List.Effectful...>2023-09-29 17:39 142K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:39 31K 
[TXT]Data.List.Membership..>2023-09-29 17:39 36K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 452K 
[TXT]Data.List.Membership..>2023-09-29 17:39 227K 
[TXT]Data.List.Relation.B..>2023-09-29 17:39 6.3K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 15K 
[TXT]Data.List.Membership..>2023-09-29 17:39 202K 
[TXT]Data.List.Extrema.html 2023-09-29 17:39 132K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:39 54K 
[TXT]Data.List.Relation.U..>2023-09-29 17:39 411K 
[TXT]Data.Vec.Bounded.Bas..>2023-09-29 17:39 68K 
[TXT]Data.Vec.html 2023-09-29 17:39 12K 
[TXT]Equality.Instances-r..>2023-09-29 17:39 120K 
[TXT]Nat.Solver.html 2023-09-29 17:39 59K 
[TXT]List.html 2023-09-29 17:39 265K 
[TXT]For-iterated-equalit..>2023-09-29 17:39 337K 
[TXT]Equivalence.List.html 2023-09-29 17:39 355K 
[TXT]Pullback.html 2023-09-29 17:39 102K 
[TXT]Equivalence.Path-spl..>2023-09-29 17:39 413K 
[TXT]Vec.Dependent.html 2023-09-29 17:39 47K 
[TXT]Modality.Basics.html 2023-09-29 17:39 2.1M 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 3.2K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 5.1K 
[TXT]Agda.Primitive.Cubic..>2023-09-29 17:39 24K 
[TXT]Erased.Level-1.html 2023-09-29 17:39 1.0M 
[TXT]Equality.Path.html 2023-09-29 17:39 342K 
[TXT]Equality.Path.Isomor..>2023-09-29 17:39 259K 
[TXT]Agda.Builtin.Word.html 2023-09-29 17:39 2.0K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:39 151K 
[TXT]Agda.Builtin.Float.html2023-09-29 17:39 32K 
[TXT]Agda.Builtin.Reflect..>2023-09-29 17:39 160K 
[TXT]Agda.Builtin.Strict...>2023-09-29 17:39 4.8K 
[TXT]Maybe.html 2023-09-29 17:39 52K 
[TXT]TC-monad.html 2023-09-29 17:39 170K 
[TXT]Tactic.Sigma-cong.html 2023-09-29 17:39 158K 
[TXT]Equivalence.Erased.html2023-09-29 17:39 689K 
[TXT]Erased.Level-2.html 2023-09-29 17:39 298K 
[TXT]Modality.Identity.html 2023-09-29 17:39 17K 
[TXT]Embedding.Erased.html 2023-09-29 17:39 67K 
[TXT]Double-negation.html 2023-09-29 17:39 96K 
[TXT]Modality.Left-exact...>2023-09-29 17:39 238K 
[TXT]Modality.Box-cong.html 2023-09-29 17:39 58K 
[TXT]Modality.Has-choice...>2023-09-29 17:39 861K 
[TXT]Modality.Commutes-wi..>2023-09-29 17:39 189K 
[TXT]Modality.Very-modal...>2023-09-29 17:39 250K 
[TXT]Modality.Empty-modal..>2023-09-29 17:39 150K 
[TXT]Erased.Stability.html 2023-09-29 17:39 1.0M 
[TXT]Erased.html 2023-09-29 17:39 6.1K 
[TXT]Erased.Cubical.html 2023-09-29 17:39 53K 
[TXT]Dec.html 2023-09-29 17:39 12K 
[TXT]Erased.Without-box-c..>2023-09-29 17:39 4.6K 
[TXT]Monad.State.html 2023-09-29 17:39 37K 
[TXT]Tactic.By.html 2023-09-29 17:39 145K 
[TXT]Tactic.By.Parametris..>2023-09-29 17:39 20K 
[TXT]Fin.html 2023-09-29 17:39 182K 
[TXT]Bag-equivalence.html 2023-09-29 17:39 647K 
[TXT]Vec.html 2023-09-29 17:39 35K 
[TXT]Vec.Function.html 2023-09-29 17:39 47K 
[TXT]Equality.Tactic.html 2023-09-29 17:39 129K 
[TXT]Pointed-type.html 2023-09-29 17:39 197K 
[TXT]Equality.Groupoid.html 2023-09-29 17:39 100K 
[TXT]List.All.html 2023-09-29 17:39 221K 
[TXT]List.All.Recursive.html2023-09-29 17:39 315K 
[TXT]Nat.Wrapper.html 2023-09-29 17:39 202K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 22K 
[TXT]Nat.Binary.html 2023-09-29 17:39 305K 
[TXT]Erased.With-K.html 2023-09-29 17:39 64K 
[TXT]Queue.html 2023-09-29 17:39 88K 
[TXT]Sum.html 2023-09-29 17:39 13K 
[TXT]H-level.Truncation.C..>2023-09-29 17:39 583K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:39 3.4K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 157K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 246K 
[TXT]Colimit.Sequential.V..>2023-09-29 17:39 179K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 275K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 418K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 557K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 53K 
[TXT]Queue.Truncated.html 2023-09-29 17:39 160K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 53K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:39 9.7K 
[TXT]Equality.Path.Unival..>2023-09-29 17:39 66K 
[TXT]Nat.Wrapper.Cubical...>2023-09-29 17:39 58K 
[TXT]Quotient.Families-of..>2023-09-29 17:39 484K 
[TXT]Quotient.Erased.Basi..>2023-09-29 17:39 88K 
[TXT]Quotient.html 2023-09-29 17:39 425K 
[TXT]Erased.Erased-matche..>2023-09-29 17:39 125K 
[TXT]Equality.Id.html 2023-09-29 17:39 10K 
[TXT]Agda.Builtin.Size.html 2023-09-29 17:39 4.2K 
[TXT]Prelude.Size.html 2023-09-29 17:39 3.1K 
[TXT]Conat.html 2023-09-29 17:39 432K 
[TXT]Colist.html 2023-09-29 17:39 375K 
[TXT]Function-universe.Si..>2023-09-29 17:39 28K 
[TXT]Accessibility.Erased..>2023-09-29 17:39 19K 
[TXT]M.html 2023-09-29 17:39 122K 
[TXT]Modality.Erased-matc..>2023-09-29 17:39 187K 
[TXT]Container.Indexed.html 2023-09-29 17:39 146K 
[TXT]Container.Indexed.Va..>2023-09-29 17:39 176K 
[TXT]Container.Indexed.Co..>2023-09-29 17:39 206K 
[TXT]Container.Indexed.Va..>2023-09-29 17:39 263K 
[TXT]Container.Indexed.M...>2023-09-29 17:39 577K 
[TXT]Container.Indexed.Va..>2023-09-29 17:39 73K 
[TXT]Container.Indexed.M...>2023-09-29 17:39 226K 
[TXT]Squash.Cubical.html 2023-09-29 17:39 4.4K 
[TXT]Squash.Erased-matche..>2023-09-29 17:39 9.0K 
[TXT]Squash.html 2023-09-29 17:39 251K 
[TXT]Agda.Builtin.IO.html 2023-09-29 17:39 2.4K 
[TXT]IO-monad.html 2023-09-29 17:39 10K 
[TXT]String.html 2023-09-29 17:39 8.1K 
[TXT]Squash.Irrelevance.html2023-09-29 17:39 46K 
[TXT]Finite-subset.Listed..>2023-09-29 17:39 270K 
[TXT]Equality.Path.Isomor..>2023-09-29 17:39 6.2K 
[TXT]Finite-subset.Listed..>2023-09-29 17:39 650K 
[TXT]Finite-subset.Listed..>2023-09-29 17:39 425K 
[TXT]Abstract-binding-tre..>2023-09-29 17:39 1.2M 
[TXT]Equality.Proposition..>2023-09-29 17:39 10K 
[TXT]Quotient.Higher-cons..>2023-09-29 17:39 551K 
[TXT]Interval.html 2023-09-29 17:39 34K 
[TXT]Suspension.html 2023-09-29 17:39 152K 
[TXT]Sphere.html 2023-09-29 17:39 68K 
[TXT]H-level.Truncation.html2023-09-29 17:39 285K 
[TXT]Group.html 2023-09-29 17:39 214K 
[TXT]Pointed-type.Homotop..>2023-09-29 17:39 74K 
[TXT]Pointed-type.Connect..>2023-09-29 17:39 32K 
[TXT]Eilenberg-MacLane-sp..>2023-09-29 17:39 317K 
[TXT]Queue.Quotiented.html 2023-09-29 17:39 96K 
[TXT]Modality.html 2023-09-29 17:39 12K 
[TXT]Pushout.html 2023-09-29 17:39 107K 
[TXT]Join.html 2023-09-29 17:39 266K 
[TXT]Integer.html 2023-09-29 17:39 183K 
[TXT]Group.Cyclic.html 2023-09-29 17:39 223K 
[TXT]Circle.html 2023-09-29 17:39 352K 
[TXT]Circle.Erased.html 2023-09-29 17:39 185K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:39 3.9K 
[TXT]Torus.html 2023-09-29 17:39 76K 
[TXT]Nat.Wrapper.Cubical...>2023-09-29 17:39 63K 
[TXT]Quotient.Set-truncat..>2023-09-29 17:39 598K 
[TXT]Quotient.Erased.html 2023-09-29 17:39 269K 
[TXT]Finite-subset.Listed..>2023-09-29 17:39 933K 
[TXT]Tactic.By.Path.html 2023-09-29 17:39 125K 
[TXT]Tactic.By.Id.html 2023-09-29 17:39 122K 
[TXT]Localisation.html 2023-09-29 17:39 195K 
[TXT]Nullification.html 2023-09-29 17:39 664K 
[TXT]Nullification.Modali..>2023-09-29 17:39 324K 
[TXT]Figure-of-eight.html 2023-09-29 17:39 155K 
[TXT]Integer.Quotient.html 2023-09-29 17:39 344K 
[TXT]Structure-identity-p..>2023-09-29 17:39 1.2M 
[TXT]Colimit.Sequential.E..>2023-09-29 17:39 105K 
[TXT]Colimit.Sequential.html2023-09-29 17:39 163K 
[TXT]H-level.Truncation.P..>2023-09-29 17:39 99K 
[TXT]Queue.Quotiented.Ins..>2023-09-29 17:39 61K 
[TXT]Finite-subset.Kurato..>2023-09-29 17:39 264K 
[TXT]Queue.Truncated.Inst..>2023-09-29 17:39 46K 
[TXT]Coherently-constant...>2023-09-29 17:39 257K 
[TXT]Container.html 2023-09-29 17:39 296K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 1.2M 
[TXT]Category.html 2023-09-29 17:39 799K 
[TXT]Structure-identity-p..>2023-09-29 17:39 116K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 235K 
[TXT]Container.Indexed.Al..>2023-09-29 17:39 366K 
[TXT]Container.Indexed.Va..>2023-09-29 17:39 420K 
[TXT]Tree.html 2023-09-29 17:39 64K 
[TXT]Tree-sort.Partial.html 2023-09-29 17:39 39K 
[TXT]Tree-sort.Examples.html2023-09-29 17:39 11K 
[TXT]Tree-sort.Full.html 2023-09-29 17:39 107K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 447K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 168K 
[TXT]Functor.html 2023-09-29 17:39 331K 
[TXT]Container.List.html 2023-09-29 17:39 168K 
[TXT]Records-with-with.html 2023-09-29 17:39 108K 
[TXT]Container.Tree.html 2023-09-29 17:39 93K 
[TXT]Container.Tree-sort...>2023-09-29 17:39 62K 
[TXT]Const.html 2023-09-29 17:39 30K 
[TXT]Container.Tree-sort...>2023-09-29 17:39 8.9K 
[TXT]Queue.Simple.html 2023-09-29 17:39 61K 
[TXT]Queue.Simple.Instanc..>2023-09-29 17:39 9.5K 
[TXT]Container.Stream.html 2023-09-29 17:39 55K 
[TXT]Monad.Reader.html 2023-09-29 17:39 27K 
[TXT]Nat.Eliminator.html 2023-09-29 17:39 74K 
[TXT]Queue.Bankers.html 2023-09-29 17:39 91K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 225K 
[TXT]Modality.Zero.html 2023-09-29 17:39 93K 
[TXT]Tactic.By.Parametris..>2023-09-29 17:39 59K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 146K 
[TXT]Bi-invertibility.html 2023-09-29 17:39 126K 
[TXT]Univalence-axiom.Iso..>2023-09-29 17:39 489K 
[TXT]Queue.Bankers.Instan..>2023-09-29 17:39 9.5K 
[TXT]Bi-invertibility.Era..>2023-09-29 17:39 132K 
[TXT]Vec.Data.html 2023-09-29 17:39 39K 
[TXT]Adjunction.html 2023-09-29 17:39 65K 
[TXT]Omniscience.html 2023-09-29 17:39 55K 
[TXT]Tactic.By.Propositio..>2023-09-29 17:39 121K 
[TXT]Bool.Very-stable.html 2023-09-29 17:39 85K 
[TXT]Finite-subset.Listed..>2023-09-29 17:39 338K 
[TXT]Finite-subset.Kurato..>2023-09-29 17:39 59K 

README
------------------------------------------------------------------------
-- 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