Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

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

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