Name | Last modified | Size | Description | |
---|---|---|---|---|
Parent Directory | - | |||
Accessibility.html | 2024-08-26 19:03 | 94K | ||
Agda.Builtin.Bool.html | 2024-08-26 19:03 | 3.1K | ||
Agda.Builtin.Char.html | 2024-08-26 19:03 | 4.0K | ||
Agda.Builtin.Cubical..> | 2024-08-26 19:03 | 53K | ||
Agda.Builtin.Cubical..> | 2024-08-26 19:03 | 9.7K | ||
Agda.Builtin.Cubical..> | 2024-08-26 19:03 | 53K | ||
Agda.Builtin.Cubical..> | 2024-08-26 19:03 | 3.2K | ||
Agda.Builtin.Cubical..> | 2024-08-26 19:03 | 5.1K | ||
Agda.Builtin.Equalit..> | 2024-08-26 19:03 | 2.6K | ||
Agda.Builtin.Float.html | 2024-08-26 19:03 | 32K | ||
Agda.Builtin.Int.html | 2024-08-26 19:03 | 3.4K | ||
Agda.Builtin.List.html | 2024-08-26 19:03 | 4.7K | ||
Agda.Builtin.Maybe.html | 2024-08-26 19:03 | 2.3K | ||
Agda.Builtin.Nat.html | 2024-08-26 19:03 | 23K | ||
Agda.Builtin.Reflect..> | 2024-08-26 19:03 | 163K | ||
Agda.Builtin.Sigma.html | 2024-08-26 19:03 | 3.4K | ||
Agda.Builtin.Strict...> | 2024-08-26 19:03 | 4.8K | ||
Agda.Builtin.String...> | 2024-08-26 19:03 | 10K | ||
Agda.Builtin.Unit.html | 2024-08-26 19:03 | 1.7K | ||
Agda.Builtin.Word.html | 2024-08-26 19:03 | 2.0K | ||
Agda.Primitive.Cubic..> | 2024-08-26 19:03 | 24K | ||
Agda.Primitive.html | 2024-08-26 19:03 | 5.4K | ||
Agda.css | 2024-08-26 19:03 | 1.8K | ||
Algebra.Bundles.Raw...> | 2024-08-26 19:03 | 64K | ||
Algebra.Bundles.html | 2024-08-26 19:03 | 278K | ||
Algebra.Consequences..> | 2024-08-26 19:03 | 8.2K | ||
Algebra.Consequences..> | 2024-08-26 19:03 | 48K | ||
Algebra.Consequences..> | 2024-08-26 19:03 | 179K | ||
Algebra.Construct.Li..> | 2024-08-26 19:03 | 83K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 17K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 7.3K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 18K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 13K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 56K | ||
Algebra.Construct.Na..> | 2024-08-26 19:03 | 108K | ||
Algebra.Core.html | 2024-08-26 19:03 | 3.3K | ||
Algebra.Definitions...> | 2024-08-26 19:03 | 18K | ||
Algebra.Definitions...> | 2024-08-26 19:03 | 11K | ||
Algebra.Definitions...> | 2024-08-26 19:03 | 21K | ||
Algebra.Definitions...> | 2024-08-26 19:03 | 118K | ||
Algebra.Lattice.Bund..> | 2024-08-26 19:03 | 7.2K | ||
Algebra.Lattice.Bund..> | 2024-08-26 19:03 | 51K | ||
Algebra.Lattice.Cons..> | 2024-08-26 19:03 | 4.5K | ||
Algebra.Lattice.Cons..> | 2024-08-26 19:03 | 18K | ||
Algebra.Lattice.Cons..> | 2024-08-26 19:03 | 6.3K | ||
Algebra.Lattice.Prop..> | 2024-08-26 19:03 | 291K | ||
Algebra.Lattice.Prop..> | 2024-08-26 19:03 | 6.0K | ||
Algebra.Lattice.Prop..> | 2024-08-26 19:03 | 42K | ||
Algebra.Lattice.Prop..> | 2024-08-26 19:03 | 11K | ||
Algebra.Lattice.Stru..> | 2024-08-26 19:03 | 39K | ||
Algebra.Morphism.Def..> | 2024-08-26 19:03 | 11K | ||
Algebra.Morphism.Str..> | 2024-08-26 19:03 | 204K | ||
Algebra.Morphism.html | 2024-08-26 19:03 | 47K | ||
Algebra.Properties.A..> | 2024-08-26 19:03 | 13K | ||
Algebra.Properties.C..> | 2024-08-26 19:03 | 112K | ||
Algebra.Properties.G..> | 2024-08-26 19:03 | 70K | ||
Algebra.Properties.L..> | 2024-08-26 19:03 | 21K | ||
Algebra.Properties.M..> | 2024-08-26 19:03 | 32K | ||
Algebra.Properties.Q..> | 2024-08-26 19:03 | 17K | ||
Algebra.Properties.R..> | 2024-08-26 19:03 | 6.4K | ||
Algebra.Properties.R..> | 2024-08-26 19:03 | 43K | ||
Algebra.Properties.S..> | 2024-08-26 19:03 | 8.2K | ||
Algebra.Properties.S..> | 2024-08-26 19:03 | 38K | ||
Algebra.Solver.Ring...> | 2024-08-26 19:03 | 43K | ||
Algebra.Solver.Ring...> | 2024-08-26 19:03 | 96K | ||
Algebra.Solver.Ring...> | 2024-08-26 19:03 | 4.3K | ||
Algebra.Solver.Ring...> | 2024-08-26 19:03 | 294K | ||
Algebra.Structures.B..> | 2024-08-26 19:03 | 65K | ||
Algebra.Structures.html | 2024-08-26 19:03 | 230K | ||
Algebra.html | 2024-08-26 19:03 | 1.9K | ||
Axiom.Extensionality..> | 2024-08-26 19:03 | 21K | ||
Axiom.UniquenessOfId..> | 2024-08-26 19:03 | 20K | ||
Bi-invertibility.Era..> | 2024-08-26 19:03 | 132K | ||
Bi-invertibility.html | 2024-08-26 19:03 | 126K | ||
Bijection.html | 2024-08-26 19:03 | 226K | ||
Bool.html | 2024-08-26 19:03 | 74K | ||
Category.html | 2024-08-26 19:03 | 799K | ||
Circle.Erased.html | 2024-08-26 19:03 | 185K | ||
Circle.html | 2024-08-26 19:03 | 352K | ||
Coherently-constant...> | 2024-08-26 19:03 | 257K | ||
Colimit.Sequential.E..> | 2024-08-26 19:03 | 105K | ||
Colimit.Sequential.V..> | 2024-08-26 19:03 | 179K | ||
Colimit.Sequential.html | 2024-08-26 19:03 | 163K | ||
Container.Indexed.Co..> | 2024-08-26 19:03 | 206K | ||
Container.Indexed.M...> | 2024-08-26 19:03 | 226K | ||
Container.Indexed.M...> | 2024-08-26 19:03 | 594K | ||
Container.Indexed.Va..> | 2024-08-26 19:03 | 263K | ||
Container.Indexed.Va..> | 2024-08-26 19:03 | 73K | ||
Container.Indexed.Va..> | 2024-08-26 19:03 | 176K | ||
Container.Indexed.html | 2024-08-26 19:03 | 146K | ||
Data.Bool.Base.html | 2024-08-26 19:03 | 13K | ||
Data.Bool.Properties..> | 2024-08-26 19:03 | 201K | ||
Data.Empty.Polymorph..> | 2024-08-26 19:03 | 3.8K | ||
Data.Empty.html | 2024-08-26 19:03 | 5.0K | ||
Data.Fin.Base.html | 2024-08-26 19:03 | 114K | ||
Data.Fin.Patterns.html | 2024-08-26 19:03 | 4.3K | ||
Data.Fin.Properties...> | 2024-08-26 19:03 | 547K | ||
Data.Irrelevant.html | 2024-08-26 19:03 | 12K | ||
Data.List.Base.html | 2024-08-26 19:03 | 221K | ||
Data.List.Effectful...> | 2024-08-26 19:03 | 147K | ||
Data.List.Extrema.Co..> | 2024-08-26 19:03 | 60K | ||
Data.List.Extrema.html | 2024-08-26 19:03 | 132K | ||
Data.List.Membership..> | 2024-08-26 19:03 | 38K | ||
Data.List.Membership..> | 2024-08-26 19:03 | 202K | ||
Data.List.Membership..> | 2024-08-26 19:03 | 9.4K | ||
Data.List.Membership..> | 2024-08-26 19:03 | 227K | ||
Data.List.Membership..> | 2024-08-26 19:03 | 20K | ||
Data.List.Properties..> | 2024-08-26 19:03 | 833K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 6.7K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 50K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 31K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 37K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 128K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 2.8K | ||
Data.List.Relation.B..> | 2024-08-26 19:03 | 11K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 420K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 110K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 6.3K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 36K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 453K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 38K | ||
Data.List.Relation.U..> | 2024-08-26 19:03 | 5.7K | ||
Data.Maybe.Base.html | 2024-08-26 19:03 | 37K | ||
Data.Maybe.Relation...> | 2024-08-26 19:03 | 54K | ||
Data.Maybe.Relation...> | 2024-08-26 19:03 | 31K | ||
Data.Nat.Base.html | 2024-08-26 19:03 | 101K | ||
Data.Nat.DivMod.Core..> | 2024-08-26 19:03 | 224K | ||
Data.Nat.DivMod.html | 2024-08-26 19:03 | 356K | ||
Data.Nat.Divisibilit..> | 2024-08-26 19:03 | 16K | ||
Data.Nat.Divisibilit..> | 2024-08-26 19:03 | 170K | ||
Data.Nat.Generalised..> | 2024-08-26 19:03 | 68K | ||
Data.Nat.Induction.html | 2024-08-26 19:03 | 24K | ||
Data.Nat.Properties...> | 2024-08-26 19:03 | 933K | ||
Data.Nat.Solver.html | 2024-08-26 19:03 | 2.4K | ||
Data.Parity.Base.html | 2024-08-26 19:03 | 19K | ||
Data.Product.Algebra..> | 2024-08-26 19:03 | 52K | ||
Data.Product.Base.html | 2024-08-26 19:03 | 87K | ||
Data.Product.Functio..> | 2024-08-26 19:03 | 161K | ||
Data.Product.Functio..> | 2024-08-26 19:03 | 49K | ||
Data.Product.Functio..> | 2024-08-26 19:03 | 59K | ||
Data.Product.Propert..> | 2024-08-26 19:03 | 57K | ||
Data.Product.Relatio..> | 2024-08-26 19:03 | 97K | ||
Data.Product.Relatio..> | 2024-08-26 19:03 | 5.4K | ||
Data.Sign.Base.html | 2024-08-26 19:03 | 8.9K | ||
Data.Sum.Algebra.html | 2024-08-26 19:03 | 32K | ||
Data.Sum.Base.html | 2024-08-26 19:03 | 26K | ||
Data.Sum.Function.Pr..> | 2024-08-26 19:03 | 44K | ||
Data.Sum.Function.Se..> | 2024-08-26 19:03 | 71K | ||
Data.Sum.Properties...> | 2024-08-26 19:03 | 60K | ||
Data.Sum.Relation.Bi..> | 2024-08-26 19:03 | 105K | ||
Data.Sum.html | 2024-08-26 19:03 | 12K | ||
Data.These.Base.html | 2024-08-26 19:03 | 36K | ||
Data.Unit.Base.html | 2024-08-26 19:03 | 1.9K | ||
Data.Unit.Polymorphi..> | 2024-08-26 19:03 | 3.3K | ||
Data.Unit.Polymorphi..> | 2024-08-26 19:03 | 27K | ||
Data.Unit.Polymorphi..> | 2024-08-26 19:03 | 1.9K | ||
Data.Vec.Base.html | 2024-08-26 19:03 | 150K | ||
Data.Vec.Bounded.Bas..> | 2024-08-26 19:03 | 66K | ||
Data.Vec.Functional...> | 2024-08-26 19:03 | 67K | ||
Data.Vec.N-ary.html | 2024-08-26 19:03 | 92K | ||
Data.Vec.html | 2024-08-26 19:03 | 12K | ||
Dec.html | 2024-08-26 19:03 | 12K | ||
Double-negation.html | 2024-08-26 19:03 | 96K | ||
Effect.Applicative.html | 2024-08-26 19:03 | 36K | ||
Effect.Choice.html | 2024-08-26 19:03 | 4.4K | ||
Effect.Empty.html | 2024-08-26 19:03 | 3.4K | ||
Effect.Functor.html | 2024-08-26 19:03 | 13K | ||
Effect.Monad.html | 2024-08-26 19:03 | 34K | ||
Eilenberg-MacLane-sp..> | 2024-08-26 19:03 | 318K | ||
Embedding.Erased.html | 2024-08-26 19:03 | 68K | ||
Embedding.html | 2024-08-26 19:03 | 93K | ||
Equality.Decidable-U..> | 2024-08-26 19:03 | 76K | ||
Equality.Decision-pr..> | 2024-08-26 19:03 | 97K | ||
Equality.Groupoid.html | 2024-08-26 19:03 | 100K | ||
Equality.Instances-r..> | 2024-08-26 19:03 | 120K | ||
Equality.Path.Isomor..> | 2024-08-26 19:03 | 5.5K | ||
Equality.Path.Isomor..> | 2024-08-26 19:03 | 259K | ||
Equality.Path.Unival..> | 2024-08-26 19:03 | 66K | ||
Equality.Path.html | 2024-08-26 19:03 | 342K | ||
Equality.Proposition..> | 2024-08-26 19:03 | 10K | ||
Equality.Proposition..> | 2024-08-26 19:03 | 19K | ||
Equality.Tactic.html | 2024-08-26 19:03 | 129K | ||
Equality.html | 2024-08-26 19:03 | 1.0M | ||
Equivalence-relation..> | 2024-08-26 19:03 | 82K | ||
Equivalence.Contract..> | 2024-08-26 19:03 | 128K | ||
Equivalence.Erased.B..> | 2024-08-26 19:03 | 98K | ||
Equivalence.Erased.C..> | 2024-08-26 19:03 | 71K | ||
Equivalence.Erased.C..> | 2024-08-26 19:03 | 3.9K | ||
Equivalence.Erased.C..> | 2024-08-26 19:03 | 154K | ||
Equivalence.Erased.C..> | 2024-08-26 19:03 | 3.4K | ||
Equivalence.Erased.html | 2024-08-26 19:03 | 881K | ||
Equivalence.Half-adj..> | 2024-08-26 19:03 | 133K | ||
Equivalence.List.html | 2024-08-26 19:03 | 355K | ||
Equivalence.Path-spl..> | 2024-08-26 19:03 | 413K | ||
Equivalence.html | 2024-08-26 19:03 | 502K | ||
Erased.Basics.html | 2024-08-26 19:03 | 14K | ||
Erased.Box-cong-axio..> | 2024-08-26 19:03 | 7.0K | ||
Erased.Cubical.html | 2024-08-26 19:03 | 49K | ||
Erased.Level-1.html | 2024-08-26 19:03 | 1.2M | ||
Erased.Level-2.html | 2024-08-26 19:03 | 332K | ||
Erased.Stability.html | 2024-08-26 19:03 | 1.1M | ||
Erased.Without-box-c..> | 2024-08-26 19:03 | 4.6K | ||
Erased.html | 2024-08-26 19:03 | 6.2K | ||
Excluded-middle.html | 2024-08-26 19:03 | 6.6K | ||
Extensionality.html | 2024-08-26 19:03 | 189K | ||
Fin.html | 2024-08-26 19:03 | 183K | ||
For-iterated-equalit..> | 2024-08-26 19:03 | 337K | ||
Function-universe.html | 2024-08-26 19:03 | 2.6M | ||
Function.Base.html | 2024-08-26 19:03 | 76K | ||
Function.Bundles.html | 2024-08-26 19:03 | 128K | ||
Function.Consequence..> | 2024-08-26 19:03 | 11K | ||
Function.Consequence..> | 2024-08-26 19:03 | 23K | ||
Function.Consequence..> | 2024-08-26 19:03 | 35K | ||
Function.Construct.C..> | 2024-08-26 19:03 | 117K | ||
Function.Construct.I..> | 2024-08-26 19:03 | 45K | ||
Function.Construct.S..> | 2024-08-26 19:03 | 72K | ||
Function.Core.html | 2024-08-26 19:03 | 5.0K | ||
Function.Definitions..> | 2024-08-26 19:03 | 21K | ||
Function.Dependent.B..> | 2024-08-26 19:03 | 9.3K | ||
Function.Indexed.Rel..> | 2024-08-26 19:03 | 8.2K | ||
Function.Metric.Bund..> | 2024-08-26 19:03 | 37K | ||
Function.Metric.Core..> | 2024-08-26 19:03 | 2.8K | ||
Function.Metric.Defi..> | 2024-08-26 19:03 | 35K | ||
Function.Metric.Nat...> | 2024-08-26 19:03 | 28K | ||
Function.Metric.Nat...> | 2024-08-26 19:03 | 2.6K | ||
Function.Metric.Nat...> | 2024-08-26 19:03 | 17K | ||
Function.Metric.Nat...> | 2024-08-26 19:03 | 18K | ||
Function.Metric.Nat...> | 2024-08-26 19:03 | 1.8K | ||
Function.Metric.Stru..> | 2024-08-26 19:03 | 22K | ||
Function.Properties...> | 2024-08-26 19:03 | 21K | ||
Function.Properties...> | 2024-08-26 19:03 | 46K | ||
Function.Properties...> | 2024-08-26 19:03 | 53K | ||
Function.Properties...> | 2024-08-26 19:03 | 19K | ||
Function.Properties...> | 2024-08-26 19:03 | 23K | ||
Function.Related.Pro..> | 2024-08-26 19:03 | 120K | ||
Function.Related.Typ..> | 2024-08-26 19:03 | 152K | ||
Function.Structures...> | 2024-08-26 19:03 | 47K | ||
Group.Cyclic.html | 2024-08-26 19:03 | 223K | ||
Group.html | 2024-08-26 19:03 | 214K | ||
Groupoid.html | 2024-08-26 19:03 | 189K | ||
H-level.Closure.html | 2024-08-26 19:03 | 406K | ||
H-level.Truncation.C..> | 2024-08-26 19:03 | 584K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 418K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 277K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 99K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 157K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 246K | ||
H-level.Truncation.P..> | 2024-08-26 19:03 | 558K | ||
H-level.Truncation.html | 2024-08-26 19:03 | 286K | ||
H-level.html | 2024-08-26 19:03 | 53K | ||
Induction.WellFounde..> | 2024-08-26 19:03 | 94K | ||
Induction.html | 2024-08-26 19:03 | 14K | ||
Injection.html | 2024-08-26 19:03 | 18K | ||
Integer.Basics.html | 2024-08-26 19:03 | 40K | ||
Integer.html | 2024-08-26 19:03 | 183K | ||
Interval.html | 2024-08-26 19:03 | 34K | ||
Lens.Dependent.html | 2024-08-26 19:03 | 596K | ||
Lens.Non-dependent.B..> | 2024-08-26 19:03 | 39K | ||
Lens.Non-dependent.E..> | 2024-08-26 19:03 | 578K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 442K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 292K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 453K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 280K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 260K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 401K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 17K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 190K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 526K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 509K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 441K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 285K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 889K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 29K | ||
Lens.Non-dependent.H..> | 2024-08-26 19:03 | 1.0M | ||
Lens.Non-dependent.T..> | 2024-08-26 19:03 | 1.0M | ||
Lens.Non-dependent.T..> | 2024-08-26 19:03 | 1.8M | ||
Lens.Non-dependent.T..> | 2024-08-26 19:03 | 874K | ||
Lens.Non-dependent.html | 2024-08-26 19:03 | 70K | ||
Level.html | 2024-08-26 19:03 | 5.6K | ||
List.html | 2024-08-26 19:03 | 265K | ||
Logical-equivalence...> | 2024-08-26 19:03 | 50K | ||
Maybe.html | 2024-08-26 19:03 | 52K | ||
Modality.Basics.html | 2024-08-26 19:03 | 2.1M | ||
Modality.Box-cong.html | 2024-08-26 19:03 | 59K | ||
Modality.Commutes-wi..> | 2024-08-26 19:03 | 189K | ||
Modality.Empty-modal..> | 2024-08-26 19:03 | 150K | ||
Modality.Has-choice...> | 2024-08-26 19:03 | 861K | ||
Modality.Identity.html | 2024-08-26 19:03 | 17K | ||
Modality.Left-exact...> | 2024-08-26 19:03 | 238K | ||
Modality.Very-modal...> | 2024-08-26 19:03 | 251K | ||
Modality.html | 2024-08-26 19:03 | 12K | ||
Monad.Raw.html | 2024-08-26 19:03 | 18K | ||
Monad.html | 2024-08-26 19:03 | 115K | ||
Nat.Solver.html | 2024-08-26 19:03 | 59K | ||
Nat.html | 2024-08-26 19:03 | 476K | ||
Pointed-type.Connect..> | 2024-08-26 19:03 | 32K | ||
Pointed-type.Homotop..> | 2024-08-26 19:03 | 74K | ||
Pointed-type.html | 2024-08-26 19:03 | 198K | ||
Preimage.html | 2024-08-26 19:03 | 59K | ||
Prelude.html | 2024-08-26 19:03 | 123K | ||
Pullback.html | 2024-08-26 19:03 | 102K | ||
Quotient.Erased.Basi..> | 2024-08-26 19:03 | 88K | ||
Quotient.Families-of..> | 2024-08-26 19:03 | 484K | ||
Quotient.html | 2024-08-26 19:03 | 425K | ||
Records-with-with.html | 2024-08-26 19:03 | 108K | ||
Relation.Binary.Bund..> | 2024-08-26 19:03 | 86K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 101K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 49K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 77K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 81K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 80K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 73K | ||
Relation.Binary.Cons..> | 2024-08-26 19:03 | 87K | ||
Relation.Binary.Core..> | 2024-08-26 19:03 | 19K | ||
Relation.Binary.Defi..> | 2024-08-26 19:03 | 98K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 11K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 16K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 13K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 9.8K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 13K | ||
Relation.Binary.Inde..> | 2024-08-26 19:03 | 2.1K | ||
Relation.Binary.Latt..> | 2024-08-26 19:03 | 69K | ||
Relation.Binary.Latt..> | 2024-08-26 19:03 | 12K | ||
Relation.Binary.Latt..> | 2024-08-26 19:03 | 62K | ||
Relation.Binary.Latt..> | 2024-08-26 19:03 | 1.7K | ||
Relation.Binary.Morp..> | 2024-08-26 19:03 | 6.3K | ||
Relation.Binary.Morp..> | 2024-08-26 19:03 | 38K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 16K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 34K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 10K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 24K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 17K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 7.0K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 35K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 109K | ||
Relation.Binary.Prop..> | 2024-08-26 19:03 | 50K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 32K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 14K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 54K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 3.7K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 5.4K | ||
Relation.Binary.Reas..> | 2024-08-26 19:03 | 90K | ||
Relation.Binary.Refl..> | 2024-08-26 19:03 | 37K | ||
Relation.Binary.Stru..> | 2024-08-26 19:03 | 9.5K | ||
Relation.Binary.Stru..> | 2024-08-26 19:03 | 64K | ||
Relation.Binary.html | 2024-08-26 19:03 | 2.1K | ||
Relation.Nullary.Dec..> | 2024-08-26 19:03 | 67K | ||
Relation.Nullary.Dec..> | 2024-08-26 19:03 | 34K | ||
Relation.Nullary.Ind..> | 2024-08-26 19:03 | 3.2K | ||
Relation.Nullary.Neg..> | 2024-08-26 19:03 | 20K | ||
Relation.Nullary.Neg..> | 2024-08-26 19:03 | 38K | ||
Relation.Nullary.Rec..> | 2024-08-26 19:03 | 18K | ||
Relation.Nullary.Ref..> | 2024-08-26 19:03 | 42K | ||
Relation.Nullary.html | 2024-08-26 19:03 | 6.3K | ||
Relation.Unary.Predi..> | 2024-08-26 19:03 | 44K | ||
Relation.Unary.Prope..> | 2024-08-26 19:03 | 114K | ||
Relation.Unary.html | 2024-08-26 19:03 | 93K | ||
Sphere.html | 2024-08-26 19:03 | 68K | ||
Surjection.html | 2024-08-26 19:03 | 88K | ||
Suspension.html | 2024-08-26 19:03 | 152K | ||
TC-monad.html | 2024-08-26 19:03 | 171K | ||
Tactic.Sigma-cong.html | 2024-08-26 19:03 | 159K | ||
Univalence-axiom.html | 2024-08-26 19:03 | 706K | ||
Vec.Dependent.html | 2024-08-26 19:03 | 47K | ||
------------------------------------------------------------------------ -- Non-dependent and dependent lenses -- Nils Anders Danielsson ------------------------------------------------------------------------ {-# OPTIONS --cubical --guardedness #-} module README where -- Non-dependent lenses. import Lens.Non-dependent import Lens.Non-dependent.Traditional import Lens.Non-dependent.Traditional.Combinators import Lens.Non-dependent.Higher import Lens.Non-dependent.Higher.Combinators import Lens.Non-dependent.Higher.Capriotti.Variant import Lens.Non-dependent.Higher.Capriotti import Lens.Non-dependent.Higher.Coherently.Not-coinductive import Lens.Non-dependent.Higher.Coherently.Coinductive import Lens.Non-dependent.Higher.Coinductive import Lens.Non-dependent.Higher.Coinductive.Small import Lens.Non-dependent.Higher.Surjective-remainder import Lens.Non-dependent.Equivalent-preimages import Lens.Non-dependent.Bijection -- Non-dependent lenses with erased proofs. import Lens.Non-dependent.Traditional.Erased import Lens.Non-dependent.Higher.Erased import Lens.Non-dependent.Higher.Capriotti.Variant.Erased import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant import Lens.Non-dependent.Higher.Coinductive.Erased import Lens.Non-dependent.Higher.Coinductive.Small.Erased import Lens.Non-dependent.Higher.Coherently.Coinductive.Erased -- Dependent lenses. import Lens.Dependent -- Comparisons of different kinds of lenses, focusing on the -- definition of composable record getters and setters. import README.Record-getters-and-setters -- Some code suggesting that types used in "programs" might not -- necessarily be sets. (If lenses are only used in programs, and -- types used in programs are always sets, then higher lenses might be -- pointless.) import README.Not-a-set -- Pointers to code corresponding to many definitions and results from -- the paper "Higher Lenses" by Paolo Capriotti, Nils Anders -- Danielsson and Andrea Vezzosi. import README.Higher-Lenses -- The lenses fst and snd. import README.Fst-snd -- Pointers to code corresponding to some definitions and results from -- the paper "Compiling Programs with Erased Univalence" by Andreas -- Abel, Nils Anders Danielsson and Andrea Vezzosi. import README.Compiling-Programs-with-Erased-Univalence