diff --git a/Agda.Builtin.Bool.html b/Agda.Builtin.Bool.html index eb90c7b..2fc74fa 100644 --- a/Agda.Builtin.Bool.html +++ b/Agda.Builtin.Bool.html @@ -1,5 +1,5 @@ -Agda.Builtin.BoolSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+Agda.Builtin.BoolSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
             --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Bool where
diff --git a/Agda.Builtin.Char.Properties.html b/Agda.Builtin.Char.Properties.html
index bc6c05f..e74453e 100644
--- a/Agda.Builtin.Char.Properties.html
+++ b/Agda.Builtin.Char.Properties.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.Char.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.Char.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Char.Properties where
 
diff --git a/Agda.Builtin.Char.html b/Agda.Builtin.Char.html
index c2912fb..49fee64 100644
--- a/Agda.Builtin.Char.html
+++ b/Agda.Builtin.Char.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.CharSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+Agda.Builtin.CharSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
             --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Char where
diff --git a/Agda.Builtin.Equality.html b/Agda.Builtin.Equality.html
index d59387d..8c1c58d 100644
--- a/Agda.Builtin.Equality.html
+++ b/Agda.Builtin.Equality.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.EqualitySource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.EqualitySource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Equality where
 
diff --git a/Agda.Builtin.Float.Properties.html b/Agda.Builtin.Float.Properties.html
index d6df434..9c21992 100644
--- a/Agda.Builtin.Float.Properties.html
+++ b/Agda.Builtin.Float.Properties.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.Float.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.Float.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Float.Properties where
 
diff --git a/Agda.Builtin.Float.html b/Agda.Builtin.Float.html
index ea850ca..2e27505 100644
--- a/Agda.Builtin.Float.html
+++ b/Agda.Builtin.Float.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.FloatSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.FloatSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Float where
 
diff --git a/Agda.Builtin.Int.html b/Agda.Builtin.Int.html
index 2f37c92..6b674dd 100644
--- a/Agda.Builtin.Int.html
+++ b/Agda.Builtin.Int.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.IntSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.IntSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Int where
 
diff --git a/Agda.Builtin.List.html b/Agda.Builtin.List.html
index 93decd4..3156989 100644
--- a/Agda.Builtin.List.html
+++ b/Agda.Builtin.List.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.ListSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.ListSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.List where
 
diff --git a/Agda.Builtin.Maybe.html b/Agda.Builtin.Maybe.html
index f9454e0..7de3f71 100644
--- a/Agda.Builtin.Maybe.html
+++ b/Agda.Builtin.Maybe.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.MaybeSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.MaybeSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Maybe where
 
diff --git a/Agda.Builtin.Nat.html b/Agda.Builtin.Nat.html
index 9e45b62..0968c1b 100644
--- a/Agda.Builtin.Nat.html
+++ b/Agda.Builtin.Nat.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.NatSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+Agda.Builtin.NatSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
             --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Nat where
diff --git a/Agda.Builtin.Reflection.Properties.html b/Agda.Builtin.Reflection.Properties.html
index 2ff4471..6ac5ff9 100644
--- a/Agda.Builtin.Reflection.Properties.html
+++ b/Agda.Builtin.Reflection.Properties.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.Reflection.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.Reflection.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Reflection.Properties where
 
diff --git a/Agda.Builtin.Reflection.html b/Agda.Builtin.Reflection.html
index a374b2a..a2c67e9 100644
--- a/Agda.Builtin.Reflection.html
+++ b/Agda.Builtin.Reflection.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.ReflectionSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.ReflectionSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Reflection where
 
diff --git a/Agda.Builtin.Sigma.html b/Agda.Builtin.Sigma.html
index 2a4343c..00de17e 100644
--- a/Agda.Builtin.Sigma.html
+++ b/Agda.Builtin.Sigma.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.SigmaSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.SigmaSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Sigma where
 
diff --git a/Agda.Builtin.Strict.html b/Agda.Builtin.Strict.html
index 24dd272..13beedc 100644
--- a/Agda.Builtin.Strict.html
+++ b/Agda.Builtin.Strict.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.StrictSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.StrictSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Strict where
 
diff --git a/Agda.Builtin.String.Properties.html b/Agda.Builtin.String.Properties.html
index 10fa79a..9bd8434 100644
--- a/Agda.Builtin.String.Properties.html
+++ b/Agda.Builtin.String.Properties.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.String.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.String.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.String.Properties where
 
diff --git a/Agda.Builtin.String.html b/Agda.Builtin.String.html
index c4a0dd9..fece67a 100644
--- a/Agda.Builtin.String.html
+++ b/Agda.Builtin.String.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.StringSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.StringSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.String where
 
diff --git a/Agda.Builtin.Unit.html b/Agda.Builtin.Unit.html
index b735b97..9a4478d 100644
--- a/Agda.Builtin.Unit.html
+++ b/Agda.Builtin.Unit.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.UnitSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+Agda.Builtin.UnitSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
             --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Unit where
diff --git a/Agda.Builtin.Word.Properties.html b/Agda.Builtin.Word.Properties.html
index 49ae049..ba7c9ef 100644
--- a/Agda.Builtin.Word.Properties.html
+++ b/Agda.Builtin.Word.Properties.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.Word.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
+Agda.Builtin.Word.PropertiesSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Word.Properties where
 
diff --git a/Agda.Builtin.Word.html b/Agda.Builtin.Word.html
index c0b77f7..9b951e6 100644
--- a/Agda.Builtin.Word.html
+++ b/Agda.Builtin.Word.html
@@ -1,5 +1,5 @@
 
-Agda.Builtin.WordSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
+Agda.Builtin.WordSource code on Github
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
             --no-sized-types --no-guardedness --level-universe #-}
 
 module Agda.Builtin.Word where
diff --git a/Agda.Primitive.html b/Agda.Primitive.html
index 9a10fd4..6023b94 100644
--- a/Agda.Primitive.html
+++ b/Agda.Primitive.html
@@ -1,5 +1,5 @@
 
-Agda.PrimitiveSource code on Github
-- The Agda primitives (preloaded).
+Agda.PrimitiveSource code on Github
-- The Agda primitives (preloaded).
 
 {-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
 
diff --git a/Algebra.Apartness.Bundles.html b/Algebra.Apartness.Bundles.html
index ac225b5..954e8ce 100644
--- a/Algebra.Apartness.Bundles.html
+++ b/Algebra.Apartness.Bundles.html
@@ -1,5 +1,5 @@
 
-Algebra.Apartness.BundlesSource code on Github
------------------------------------------------------------------------
+Algebra.Apartness.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for local algebraic structures
diff --git a/Algebra.Apartness.Structures.html b/Algebra.Apartness.Structures.html
index 6f0b1c9..ee67ebe 100644
--- a/Algebra.Apartness.Structures.html
+++ b/Algebra.Apartness.Structures.html
@@ -1,5 +1,5 @@
 
-Algebra.Apartness.StructuresSource code on Github
------------------------------------------------------------------------
+Algebra.Apartness.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Algebraic structures with an apartness relation
diff --git a/Algebra.Apartness.html b/Algebra.Apartness.html
index 5f831b5..e177a37 100644
--- a/Algebra.Apartness.html
+++ b/Algebra.Apartness.html
@@ -1,5 +1,5 @@
 
-Algebra.ApartnessSource code on Github
------------------------------------------------------------------------
+Algebra.ApartnessSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Algebraic objects with an apartness relation
diff --git a/Algebra.Bundles.Raw.html b/Algebra.Bundles.Raw.html
index e37dfc9..fc87406 100644
--- a/Algebra.Bundles.Raw.html
+++ b/Algebra.Bundles.Raw.html
@@ -1,5 +1,5 @@
 
-Algebra.Bundles.RawSource code on Github
------------------------------------------------------------------------
+Algebra.Bundles.RawSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of 'raw' bundles
diff --git a/Algebra.Bundles.html b/Algebra.Bundles.html
index 2a2e0c8..f30f632 100644
--- a/Algebra.Bundles.html
+++ b/Algebra.Bundles.html
@@ -1,5 +1,5 @@
 
-Algebra.BundlesSource code on Github
------------------------------------------------------------------------
+Algebra.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of algebraic structures like monoids and rings
diff --git a/Algebra.Consequences.Base.html b/Algebra.Consequences.Base.html
index fd945e6..8bc80b8 100644
--- a/Algebra.Consequences.Base.html
+++ b/Algebra.Consequences.Base.html
@@ -1,5 +1,5 @@
 
-Algebra.Consequences.BaseSource code on Github
------------------------------------------------------------------------
+Algebra.Consequences.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lemmas relating algebraic definitions (such as associativity and
diff --git a/Algebra.Consequences.Propositional.html b/Algebra.Consequences.Propositional.html
index ede808b..bd44190 100644
--- a/Algebra.Consequences.Propositional.html
+++ b/Algebra.Consequences.Propositional.html
@@ -1,5 +1,5 @@
 
-Algebra.Consequences.PropositionalSource code on Github
------------------------------------------------------------------------
+Algebra.Consequences.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relations between properties of functions, such as associativity and
diff --git a/Algebra.Consequences.Setoid.html b/Algebra.Consequences.Setoid.html
index a524b22..ab0ba47 100644
--- a/Algebra.Consequences.Setoid.html
+++ b/Algebra.Consequences.Setoid.html
@@ -1,5 +1,5 @@
 
-Algebra.Consequences.SetoidSource code on Github
------------------------------------------------------------------------
+Algebra.Consequences.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relations between properties of functions, such as associativity and
diff --git a/Algebra.Construct.LiftedChoice.html b/Algebra.Construct.LiftedChoice.html
index 6be4e4c..b5f7f72 100644
--- a/Algebra.Construct.LiftedChoice.html
+++ b/Algebra.Construct.LiftedChoice.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.LiftedChoiceSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.LiftedChoiceSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Choosing between elements based on the result of applying a function
diff --git a/Algebra.Construct.NaturalChoice.Base.html b/Algebra.Construct.NaturalChoice.Base.html
index 366dc14..eb00396 100644
--- a/Algebra.Construct.NaturalChoice.Base.html
+++ b/Algebra.Construct.NaturalChoice.Base.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.BaseSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic definition of an operator that computes the min/max value
diff --git a/Algebra.Construct.NaturalChoice.Max.html b/Algebra.Construct.NaturalChoice.Max.html
index 647d35c..4a2e30f 100644
--- a/Algebra.Construct.NaturalChoice.Max.html
+++ b/Algebra.Construct.NaturalChoice.Max.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.MaxSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.MaxSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The max operator derived from an arbitrary total preorder.
diff --git a/Algebra.Construct.NaturalChoice.MaxOp.html b/Algebra.Construct.NaturalChoice.MaxOp.html
index 95c7e97..93df7fb 100644
--- a/Algebra.Construct.NaturalChoice.MaxOp.html
+++ b/Algebra.Construct.NaturalChoice.MaxOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.MaxOpSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.MaxOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of a max operator derived from a spec over a total
diff --git a/Algebra.Construct.NaturalChoice.Min.html b/Algebra.Construct.NaturalChoice.Min.html
index a88bed2..b396bb3 100644
--- a/Algebra.Construct.NaturalChoice.Min.html
+++ b/Algebra.Construct.NaturalChoice.Min.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.MinSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.MinSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The min operator derived from an arbitrary total preorder.
diff --git a/Algebra.Construct.NaturalChoice.MinMaxOp.html b/Algebra.Construct.NaturalChoice.MinMaxOp.html
index bad9fa8..8324f3c 100644
--- a/Algebra.Construct.NaturalChoice.MinMaxOp.html
+++ b/Algebra.Construct.NaturalChoice.MinMaxOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.MinMaxOpSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.MinMaxOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of min and max operators specified over a total
diff --git a/Algebra.Construct.NaturalChoice.MinOp.html b/Algebra.Construct.NaturalChoice.MinOp.html
index 28c813a..c22a593 100644
--- a/Algebra.Construct.NaturalChoice.MinOp.html
+++ b/Algebra.Construct.NaturalChoice.MinOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Construct.NaturalChoice.MinOpSource code on Github
------------------------------------------------------------------------
+Algebra.Construct.NaturalChoice.MinOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of a min operator derived from a spec over a total
diff --git a/Algebra.Core.html b/Algebra.Core.html
index ef8d2a0..a657c86 100644
--- a/Algebra.Core.html
+++ b/Algebra.Core.html
@@ -1,5 +1,5 @@
 
-Algebra.CoreSource code on Github
------------------------------------------------------------------------
+Algebra.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core algebraic definitions
diff --git a/Algebra.Definitions.RawMagma.html b/Algebra.Definitions.RawMagma.html
index 94fce38..89bf685 100644
--- a/Algebra.Definitions.RawMagma.html
+++ b/Algebra.Definitions.RawMagma.html
@@ -1,5 +1,5 @@
 
-Algebra.Definitions.RawMagmaSource code on Github
------------------------------------------------------------------------
+Algebra.Definitions.RawMagmaSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic auxiliary definitions for magma-like structures
diff --git a/Algebra.Definitions.RawMonoid.html b/Algebra.Definitions.RawMonoid.html
index 7a7561f..7048558 100644
--- a/Algebra.Definitions.RawMonoid.html
+++ b/Algebra.Definitions.RawMonoid.html
@@ -1,5 +1,5 @@
 
-Algebra.Definitions.RawMonoidSource code on Github
------------------------------------------------------------------------
+Algebra.Definitions.RawMonoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic auxiliary definitions for monoid-like structures
diff --git a/Algebra.Definitions.RawSemiring.html b/Algebra.Definitions.RawSemiring.html
index 5cb2d66..dd598ff 100644
--- a/Algebra.Definitions.RawSemiring.html
+++ b/Algebra.Definitions.RawSemiring.html
@@ -1,5 +1,5 @@
 
-Algebra.Definitions.RawSemiringSource code on Github
------------------------------------------------------------------------
+Algebra.Definitions.RawSemiringSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic auxiliary definitions for semiring-like structures
diff --git a/Algebra.Definitions.html b/Algebra.Definitions.html
index f202990..f5e5ae6 100644
--- a/Algebra.Definitions.html
+++ b/Algebra.Definitions.html
@@ -1,5 +1,5 @@
 
-Algebra.DefinitionsSource code on Github
------------------------------------------------------------------------
+Algebra.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of functions, such as associativity and commutativity
diff --git a/Algebra.Lattice.Bundles.Raw.html b/Algebra.Lattice.Bundles.Raw.html
index 4852e55..50d1059 100644
--- a/Algebra.Lattice.Bundles.Raw.html
+++ b/Algebra.Lattice.Bundles.Raw.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Bundles.RawSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Bundles.RawSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of 'raw' bundles
diff --git a/Algebra.Lattice.Bundles.html b/Algebra.Lattice.Bundles.html
index 28718a9..4f99add 100644
--- a/Algebra.Lattice.Bundles.html
+++ b/Algebra.Lattice.Bundles.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.BundlesSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of algebraic structures like semilattices and lattices
diff --git a/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html b/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html
index 74e6a23..4ac238e 100644
--- a/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html
+++ b/Algebra.Lattice.Construct.NaturalChoice.MaxOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Construct.NaturalChoice.MaxOpSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Construct.NaturalChoice.MaxOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of a max operator derived from a spec over a total
diff --git a/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html b/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html
index 1014568..b2baae5 100644
--- a/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html
+++ b/Algebra.Lattice.Construct.NaturalChoice.MinMaxOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Construct.NaturalChoice.MinMaxOpSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Construct.NaturalChoice.MinMaxOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of min and max operators specified over a total preorder.
diff --git a/Algebra.Lattice.Construct.NaturalChoice.MinOp.html b/Algebra.Lattice.Construct.NaturalChoice.MinOp.html
index 473d630..9620096 100644
--- a/Algebra.Lattice.Construct.NaturalChoice.MinOp.html
+++ b/Algebra.Lattice.Construct.NaturalChoice.MinOp.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Construct.NaturalChoice.MinOpSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Construct.NaturalChoice.MinOpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of a min operator derived from a spec over a total
diff --git a/Algebra.Lattice.Morphism.LatticeMonomorphism.html b/Algebra.Lattice.Morphism.LatticeMonomorphism.html
index e57d87a..5b7969e 100644
--- a/Algebra.Lattice.Morphism.LatticeMonomorphism.html
+++ b/Algebra.Lattice.Morphism.LatticeMonomorphism.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Morphism.LatticeMonomorphismSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Morphism.LatticeMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between lattice-like structures
diff --git a/Algebra.Lattice.Morphism.Structures.html b/Algebra.Lattice.Morphism.Structures.html
index 2998c01..0fe4cec 100644
--- a/Algebra.Lattice.Morphism.Structures.html
+++ b/Algebra.Lattice.Morphism.Structures.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Morphisms between algebraic lattice structures
diff --git a/Algebra.Lattice.Properties.BooleanAlgebra.html b/Algebra.Lattice.Properties.BooleanAlgebra.html
index f6228ef..25cc77f 100644
--- a/Algebra.Lattice.Properties.BooleanAlgebra.html
+++ b/Algebra.Lattice.Properties.BooleanAlgebra.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Properties.BooleanAlgebraSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Properties.BooleanAlgebraSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties of Boolean algebras
diff --git a/Algebra.Lattice.Properties.DistributiveLattice.html b/Algebra.Lattice.Properties.DistributiveLattice.html
index 5a7d7ef..b9418d9 100644
--- a/Algebra.Lattice.Properties.DistributiveLattice.html
+++ b/Algebra.Lattice.Properties.DistributiveLattice.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Properties.DistributiveLatticeSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Properties.DistributiveLatticeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties
diff --git a/Algebra.Lattice.Properties.Lattice.html b/Algebra.Lattice.Properties.Lattice.html
index 965eb4d..e337021 100644
--- a/Algebra.Lattice.Properties.Lattice.html
+++ b/Algebra.Lattice.Properties.Lattice.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Properties.LatticeSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Properties.LatticeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties of lattices
diff --git a/Algebra.Lattice.Properties.Semilattice.html b/Algebra.Lattice.Properties.Semilattice.html
index 8ddb12e..3e070bd 100644
--- a/Algebra.Lattice.Properties.Semilattice.html
+++ b/Algebra.Lattice.Properties.Semilattice.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Properties.SemilatticeSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Properties.SemilatticeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties of semilattices
diff --git a/Algebra.Lattice.Structures.Biased.html b/Algebra.Lattice.Structures.Biased.html
index b5f1d85..6366b5b 100644
--- a/Algebra.Lattice.Structures.Biased.html
+++ b/Algebra.Lattice.Structures.Biased.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.Structures.BiasedSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.Structures.BiasedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some biased records for lattice-like structures. Such records are
diff --git a/Algebra.Lattice.Structures.html b/Algebra.Lattice.Structures.html
index 43c9c3a..9c8ccd7 100644
--- a/Algebra.Lattice.Structures.html
+++ b/Algebra.Lattice.Structures.html
@@ -1,5 +1,5 @@
 
-Algebra.Lattice.StructuresSource code on Github
------------------------------------------------------------------------
+Algebra.Lattice.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some lattice-like structures defined by properties of _∧_ and _∨_
diff --git a/Algebra.Lattice.html b/Algebra.Lattice.html
index c17014f..b5890a4 100644
--- a/Algebra.Lattice.html
+++ b/Algebra.Lattice.html
@@ -1,5 +1,5 @@
 
-Algebra.LatticeSource code on Github
------------------------------------------------------------------------
+Algebra.LatticeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of algebraic structures like semilattices and lattices
diff --git a/Algebra.Morphism.Definitions.html b/Algebra.Morphism.Definitions.html
index 28db280..dd1309b 100644
--- a/Algebra.Morphism.Definitions.html
+++ b/Algebra.Morphism.Definitions.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.DefinitionsSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic definitions for morphisms between algebraic structures
diff --git a/Algebra.Morphism.GroupMonomorphism.html b/Algebra.Morphism.GroupMonomorphism.html
index 759345a..4d3f07a 100644
--- a/Algebra.Morphism.GroupMonomorphism.html
+++ b/Algebra.Morphism.GroupMonomorphism.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.GroupMonomorphismSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.GroupMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between group-like structures
diff --git a/Algebra.Morphism.MagmaMonomorphism.html b/Algebra.Morphism.MagmaMonomorphism.html
index ebb9b5e..e7fd3bd 100644
--- a/Algebra.Morphism.MagmaMonomorphism.html
+++ b/Algebra.Morphism.MagmaMonomorphism.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.MagmaMonomorphismSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.MagmaMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between magma-like structures
diff --git a/Algebra.Morphism.MonoidMonomorphism.html b/Algebra.Morphism.MonoidMonomorphism.html
index 2e3254c..2074b51 100644
--- a/Algebra.Morphism.MonoidMonomorphism.html
+++ b/Algebra.Morphism.MonoidMonomorphism.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.MonoidMonomorphismSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.MonoidMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between monoid-like structures
diff --git a/Algebra.Morphism.RingMonomorphism.html b/Algebra.Morphism.RingMonomorphism.html
index 49074e6..cecce87 100644
--- a/Algebra.Morphism.RingMonomorphism.html
+++ b/Algebra.Morphism.RingMonomorphism.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.RingMonomorphismSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.RingMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between ring-like structures
diff --git a/Algebra.Morphism.Structures.html b/Algebra.Morphism.Structures.html
index 3229e3e..7cdd185 100644
--- a/Algebra.Morphism.Structures.html
+++ b/Algebra.Morphism.Structures.html
@@ -1,5 +1,5 @@
 
-Algebra.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
+Algebra.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Morphisms between algebraic structures
diff --git a/Algebra.Morphism.html b/Algebra.Morphism.html
index 767f192..5b3f3c7 100644
--- a/Algebra.Morphism.html
+++ b/Algebra.Morphism.html
@@ -1,5 +1,5 @@
 
-Algebra.MorphismSource code on Github
------------------------------------------------------------------------
+Algebra.MorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Morphisms between algebraic structures
diff --git a/Algebra.Properties.AbelianGroup.html b/Algebra.Properties.AbelianGroup.html
index 072ad42..5f41f20 100644
--- a/Algebra.Properties.AbelianGroup.html
+++ b/Algebra.Properties.AbelianGroup.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.AbelianGroupSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.AbelianGroupSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties
diff --git a/Algebra.Properties.CommutativeSemigroup.html b/Algebra.Properties.CommutativeSemigroup.html
index 7395e83..106f54e 100644
--- a/Algebra.Properties.CommutativeSemigroup.html
+++ b/Algebra.Properties.CommutativeSemigroup.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.CommutativeSemigroupSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.CommutativeSemigroupSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some theory for commutative semigroup
diff --git a/Algebra.Properties.Group.html b/Algebra.Properties.Group.html
index 09f191e..cf5c45b 100644
--- a/Algebra.Properties.Group.html
+++ b/Algebra.Properties.Group.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.GroupSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.GroupSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some derivable properties
diff --git a/Algebra.Properties.Loop.html b/Algebra.Properties.Loop.html
index b848eff..50015b2 100644
--- a/Algebra.Properties.Loop.html
+++ b/Algebra.Properties.Loop.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.LoopSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.LoopSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some basic properties of Loop
diff --git a/Algebra.Properties.Monoid.Mult.html b/Algebra.Properties.Monoid.Mult.html
index eec988d..1e98b37 100644
--- a/Algebra.Properties.Monoid.Mult.html
+++ b/Algebra.Properties.Monoid.Mult.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.Monoid.MultSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.Monoid.MultSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Multiplication over a monoid (i.e. repeated addition)
diff --git a/Algebra.Properties.Quasigroup.html b/Algebra.Properties.Quasigroup.html
index 0e28fbf..1d0e59a 100644
--- a/Algebra.Properties.Quasigroup.html
+++ b/Algebra.Properties.Quasigroup.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.QuasigroupSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.QuasigroupSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some basic properties of Quasigroup
diff --git a/Algebra.Properties.Ring.html b/Algebra.Properties.Ring.html
index 2147fa9..c24accd 100644
--- a/Algebra.Properties.Ring.html
+++ b/Algebra.Properties.Ring.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.RingSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.RingSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some basic properties of Rings
diff --git a/Algebra.Properties.RingWithoutOne.html b/Algebra.Properties.RingWithoutOne.html
index 0cdc840..5447210 100644
--- a/Algebra.Properties.RingWithoutOne.html
+++ b/Algebra.Properties.RingWithoutOne.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.RingWithoutOneSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.RingWithoutOneSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some basic properties of RingWithoutOne
diff --git a/Algebra.Properties.Semigroup.html b/Algebra.Properties.Semigroup.html
index 1d777e7..cb11cb9 100644
--- a/Algebra.Properties.Semigroup.html
+++ b/Algebra.Properties.Semigroup.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.SemigroupSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.SemigroupSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some theory for Semigroup
diff --git a/Algebra.Properties.Semiring.Exp.html b/Algebra.Properties.Semiring.Exp.html
index 00fb8f6..697b543 100644
--- a/Algebra.Properties.Semiring.Exp.html
+++ b/Algebra.Properties.Semiring.Exp.html
@@ -1,5 +1,5 @@
 
-Algebra.Properties.Semiring.ExpSource code on Github
------------------------------------------------------------------------
+Algebra.Properties.Semiring.ExpSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Exponentiation defined over a semiring as repeated multiplication
diff --git a/Algebra.Solver.Ring.AlmostCommutativeRing.html b/Algebra.Solver.Ring.AlmostCommutativeRing.html
index 34a8a7c..9536487 100644
--- a/Algebra.Solver.Ring.AlmostCommutativeRing.html
+++ b/Algebra.Solver.Ring.AlmostCommutativeRing.html
@@ -1,5 +1,5 @@
 
-Algebra.Solver.Ring.AlmostCommutativeRingSource code on Github
------------------------------------------------------------------------
+Algebra.Solver.Ring.AlmostCommutativeRingSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Commutative semirings with some additional structure ("almost"
diff --git a/Algebra.Solver.Ring.Lemmas.html b/Algebra.Solver.Ring.Lemmas.html
index d44cc90..3177f84 100644
--- a/Algebra.Solver.Ring.Lemmas.html
+++ b/Algebra.Solver.Ring.Lemmas.html
@@ -1,5 +1,5 @@
 
-Algebra.Solver.Ring.LemmasSource code on Github
------------------------------------------------------------------------
+Algebra.Solver.Ring.LemmasSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some boring lemmas used by the ring solver
diff --git a/Algebra.Solver.Ring.Simple.html b/Algebra.Solver.Ring.Simple.html
index 28bbbb9..1f32121 100644
--- a/Algebra.Solver.Ring.Simple.html
+++ b/Algebra.Solver.Ring.Simple.html
@@ -1,5 +1,5 @@
 
-Algebra.Solver.Ring.SimpleSource code on Github
------------------------------------------------------------------------
+Algebra.Solver.Ring.SimpleSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Instantiates the ring solver with two copies of the same ring with
diff --git a/Algebra.Solver.Ring.html b/Algebra.Solver.Ring.html
index f538133..bea2875 100644
--- a/Algebra.Solver.Ring.html
+++ b/Algebra.Solver.Ring.html
@@ -1,5 +1,5 @@
 
-Algebra.Solver.RingSource code on Github
------------------------------------------------------------------------
+Algebra.Solver.RingSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Old solver for commutative ring or semiring equalities
diff --git a/Algebra.Structures.Biased.html b/Algebra.Structures.Biased.html
index 55e893b..83904e0 100644
--- a/Algebra.Structures.Biased.html
+++ b/Algebra.Structures.Biased.html
@@ -1,5 +1,5 @@
 
-Algebra.Structures.BiasedSource code on Github
------------------------------------------------------------------------
+Algebra.Structures.BiasedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Ways to give instances of certain structures where some fields can
diff --git a/Algebra.Structures.html b/Algebra.Structures.html
index ff9d202..0be5194 100644
--- a/Algebra.Structures.html
+++ b/Algebra.Structures.html
@@ -1,5 +1,5 @@
 
-Algebra.StructuresSource code on Github
------------------------------------------------------------------------
+Algebra.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some algebraic structures (not packed up with sets, operations, etc.)
diff --git a/Algebra.html b/Algebra.html
index 3b0b6bb..0505cc9 100644
--- a/Algebra.html
+++ b/Algebra.html
@@ -1,5 +1,5 @@
 
-AlgebraSource code on Github
------------------------------------------------------------------------
+AlgebraSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of algebraic structures like monoids and rings
diff --git a/Axiom.Extensionality.Propositional.html b/Axiom.Extensionality.Propositional.html
index fb7ff68..90b5a94 100644
--- a/Axiom.Extensionality.Propositional.html
+++ b/Axiom.Extensionality.Propositional.html
@@ -1,5 +1,5 @@
 
-Axiom.Extensionality.PropositionalSource code on Github
------------------------------------------------------------------------
+Axiom.Extensionality.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Results concerning function extensionality for propositional equality
diff --git a/Axiom.UniquenessOfIdentityProofs.html b/Axiom.UniquenessOfIdentityProofs.html
index 232cffc..5eddf39 100644
--- a/Axiom.UniquenessOfIdentityProofs.html
+++ b/Axiom.UniquenessOfIdentityProofs.html
@@ -1,5 +1,5 @@
 
-Axiom.UniquenessOfIdentityProofsSource code on Github
------------------------------------------------------------------------
+Axiom.UniquenessOfIdentityProofsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Results concerning uniqueness of identity proofs
diff --git a/Class.Allable.Core.html b/Class.Allable.Core.html
index b1a5b2e..f024708 100644
--- a/Class.Allable.Core.html
+++ b/Class.Allable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Allable.CoreSource code on Github
module Class.Allable.Core where
+Class.Allable.CoreSource code on Github
module Class.Allable.Core where
 
 open import Class.Prelude
 
diff --git a/Class.Allable.Instance.html b/Class.Allable.Instance.html
index 768f7fc..facd32f 100644
--- a/Class.Allable.Instance.html
+++ b/Class.Allable.Instance.html
@@ -1,5 +1,5 @@
 
-Class.Allable.InstanceSource code on Github
module Class.Allable.Instance where
+Class.Allable.InstanceSource code on Github
module Class.Allable.Instance where
 
 open import Class.Prelude
 open import Class.Allable.Core
diff --git a/Class.Allable.html b/Class.Allable.html
index 291ad12..5999826 100644
--- a/Class.Allable.html
+++ b/Class.Allable.html
@@ -1,5 +1,5 @@
 
-Class.AllableSource code on Github
module Class.Allable where
+Class.AllableSource code on Github
module Class.Allable where
 
 open import Class.Allable.Core public
 open import Class.Allable.Instance public
diff --git a/Class.Anyable.Core.html b/Class.Anyable.Core.html
index dc1df1f..cb52256 100644
--- a/Class.Anyable.Core.html
+++ b/Class.Anyable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Anyable.CoreSource code on Github
module Class.Anyable.Core where
+Class.Anyable.CoreSource code on Github
module Class.Anyable.Core where
 
 open import Class.Prelude
 
diff --git a/Class.Anyable.Instance.html b/Class.Anyable.Instance.html
index 3f45979..c1696dd 100644
--- a/Class.Anyable.Instance.html
+++ b/Class.Anyable.Instance.html
@@ -1,5 +1,5 @@
 
-Class.Anyable.InstanceSource code on Github
module Class.Anyable.Instance where
+Class.Anyable.InstanceSource code on Github
module Class.Anyable.Instance where
 
 open import Class.Prelude
 open import Class.Anyable.Core
diff --git a/Class.Anyable.html b/Class.Anyable.html
index bae711b..f7654e6 100644
--- a/Class.Anyable.html
+++ b/Class.Anyable.html
@@ -1,5 +1,5 @@
 
-Class.AnyableSource code on Github
module Class.Anyable where
+Class.AnyableSource code on Github
module Class.Anyable where
 
 open import Class.Anyable.Core public
 open import Class.Anyable.Instance public
diff --git a/Class.Applicative.Core.html b/Class.Applicative.Core.html
index d28a126..dba8f97 100644
--- a/Class.Applicative.Core.html
+++ b/Class.Applicative.Core.html
@@ -1,5 +1,5 @@
 
-Class.Applicative.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Applicative.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Applicative.Core where
 
 open import Class.Prelude
diff --git a/Class.Applicative.Instances.html b/Class.Applicative.Instances.html
index 31ec4f0..e09f98e 100644
--- a/Class.Applicative.Instances.html
+++ b/Class.Applicative.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Applicative.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Applicative.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Applicative.Instances where
 
 open import Class.Prelude
diff --git a/Class.Applicative.html b/Class.Applicative.html
index 4d34ffd..8a60cbb 100644
--- a/Class.Applicative.html
+++ b/Class.Applicative.html
@@ -1,5 +1,5 @@
 
-Class.ApplicativeSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.ApplicativeSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Applicative where
 
 open import Class.Applicative.Core public
diff --git a/Class.Bifunctor.html b/Class.Bifunctor.html
index c9088f3..587ce33 100644
--- a/Class.Bifunctor.html
+++ b/Class.Bifunctor.html
@@ -1,5 +1,5 @@
 
-Class.BifunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.BifunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Bifunctor where
 
 open import Class.Prelude hiding (A; B; C)
diff --git a/Class.CommutativeMonoid.Core.html b/Class.CommutativeMonoid.Core.html
index 88b8d08..8f983d9 100644
--- a/Class.CommutativeMonoid.Core.html
+++ b/Class.CommutativeMonoid.Core.html
@@ -1,5 +1,5 @@
 
-Class.CommutativeMonoid.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.CommutativeMonoid.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.CommutativeMonoid.Core where
 
 open import Class.Prelude
diff --git a/Class.CommutativeMonoid.Instances.html b/Class.CommutativeMonoid.Instances.html
index 2e0b9c1..3f5f3f8 100644
--- a/Class.CommutativeMonoid.Instances.html
+++ b/Class.CommutativeMonoid.Instances.html
@@ -1,5 +1,5 @@
 
-Class.CommutativeMonoid.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.CommutativeMonoid.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 
 module Class.CommutativeMonoid.Instances where
 
diff --git a/Class.CommutativeMonoid.html b/Class.CommutativeMonoid.html
index 8dd9a18..76be5c8 100644
--- a/Class.CommutativeMonoid.html
+++ b/Class.CommutativeMonoid.html
@@ -1,5 +1,5 @@
 
-Class.CommutativeMonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.CommutativeMonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.CommutativeMonoid where
 
 open import Class.CommutativeMonoid.Core public
diff --git a/Class.Core.html b/Class.Core.html
index 73bdd86..0da445a 100644
--- a/Class.Core.html
+++ b/Class.Core.html
@@ -1,5 +1,5 @@
 
-Class.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Core where
 
 open import Class.Prelude
diff --git a/Class.DecEq.Core.html b/Class.DecEq.Core.html
index ae48045..7006fce 100644
--- a/Class.DecEq.Core.html
+++ b/Class.DecEq.Core.html
@@ -1,5 +1,5 @@
 
-Class.DecEq.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.DecEq.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.DecEq.Core where
 
 open import Class.Prelude
diff --git a/Class.DecEq.Instances.html b/Class.DecEq.Instances.html
index d58c743..7de928d 100644
--- a/Class.DecEq.Instances.html
+++ b/Class.DecEq.Instances.html
@@ -1,5 +1,5 @@
 
-Class.DecEq.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.DecEq.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.DecEq.Instances where
 
 open import Class.Prelude
diff --git a/Class.DecEq.WithK.html b/Class.DecEq.WithK.html
index 256e3b3..3307d41 100644
--- a/Class.DecEq.WithK.html
+++ b/Class.DecEq.WithK.html
@@ -1,5 +1,5 @@
 
-Class.DecEq.WithKSource code on Github
{-# OPTIONS --with-K #-}
+Class.DecEq.WithKSource code on Github
{-# OPTIONS --with-K #-}
 open import Class.Prelude
 open import Class.DecEq.Core
 
diff --git a/Class.DecEq.html b/Class.DecEq.html
index 6417269..13ad02e 100644
--- a/Class.DecEq.html
+++ b/Class.DecEq.html
@@ -1,5 +1,5 @@
 
-Class.DecEqSource code on Github
{-# OPTIONS --without-K #-}
+Class.DecEqSource code on Github
{-# OPTIONS --without-K #-}
 module Class.DecEq where
 
 open import Class.DecEq.Core public
diff --git a/Class.Decidable.Core.html b/Class.Decidable.Core.html
index b070fc6..d404a78 100644
--- a/Class.Decidable.Core.html
+++ b/Class.Decidable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Decidable.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Decidable.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Decidable.Core where
 
 open import Class.Prelude
diff --git a/Class.Decidable.Instances.html b/Class.Decidable.Instances.html
index c462066..4fea327 100644
--- a/Class.Decidable.Instances.html
+++ b/Class.Decidable.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Decidable.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Decidable.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Decidable.Instances where
 
 open import Class.Prelude
diff --git a/Class.Decidable.html b/Class.Decidable.html
index 577eb9b..3c79b4c 100644
--- a/Class.Decidable.html
+++ b/Class.Decidable.html
@@ -1,5 +1,5 @@
 
-Class.DecidableSource code on Github
{-# OPTIONS --without-K #-}
+Class.DecidableSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Decidable where
 
 open import Class.Decidable.Core public
diff --git a/Class.Default.html b/Class.Default.html
index 533f713..31a35c4 100644
--- a/Class.Default.html
+++ b/Class.Default.html
@@ -1,5 +1,5 @@
 
-Class.DefaultSource code on Github
------------------------------------------------------------------------
+Class.DefaultSource code on Github
------------------------------------------------------------------------
 -- Types with a default value.
 ------------------------------------------------------------------------
 
diff --git a/Class.Foldable.Core.html b/Class.Foldable.Core.html
index c58ae8d..b6ad4a5 100644
--- a/Class.Foldable.Core.html
+++ b/Class.Foldable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Foldable.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Foldable.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Foldable.Core where
 
 open import Class.Prelude
diff --git a/Class.Foldable.Instances.html b/Class.Foldable.Instances.html
index af4d44e..a63a699 100644
--- a/Class.Foldable.Instances.html
+++ b/Class.Foldable.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Foldable.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Foldable.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Foldable.Instances where
 
 open import Class.Prelude
diff --git a/Class.Foldable.html b/Class.Foldable.html
index 4b6e64c..af91944 100644
--- a/Class.Foldable.html
+++ b/Class.Foldable.html
@@ -1,5 +1,5 @@
 
-Class.FoldableSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.FoldableSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Foldable where
 
 open import Class.Foldable.Core public
diff --git a/Class.Functor.Core.html b/Class.Functor.Core.html
index 283158f..2345f54 100644
--- a/Class.Functor.Core.html
+++ b/Class.Functor.Core.html
@@ -1,5 +1,5 @@
 
-Class.Functor.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Functor.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Functor.Core where
 
 open import Class.Prelude
diff --git a/Class.Functor.Instances.html b/Class.Functor.Instances.html
index 2e155b8..99b10f0 100644
--- a/Class.Functor.Instances.html
+++ b/Class.Functor.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Functor.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Functor.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Functor.Instances where
 
 open import Class.Prelude
diff --git a/Class.Functor.html b/Class.Functor.html
index 58968f8..ecf8023 100644
--- a/Class.Functor.html
+++ b/Class.Functor.html
@@ -1,5 +1,5 @@
 
-Class.FunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.FunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Functor where
 
 open import Class.Functor.Core public
diff --git a/Class.HasAdd.Core.html b/Class.HasAdd.Core.html
index 003e6f1..b9be177 100644
--- a/Class.HasAdd.Core.html
+++ b/Class.HasAdd.Core.html
@@ -1,5 +1,5 @@
 
-Class.HasAdd.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.HasAdd.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd.Core where
 
 open import Class.Prelude
diff --git a/Class.HasAdd.Instance.html b/Class.HasAdd.Instance.html
index cf8999d..d523e44 100644
--- a/Class.HasAdd.Instance.html
+++ b/Class.HasAdd.Instance.html
@@ -1,5 +1,5 @@
 
-Class.HasAdd.InstanceSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.HasAdd.InstanceSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd.Instance where
 
 open import Class.HasAdd.Core
diff --git a/Class.HasAdd.html b/Class.HasAdd.html
index fe0470e..8c68506 100644
--- a/Class.HasAdd.html
+++ b/Class.HasAdd.html
@@ -1,5 +1,5 @@
 
-Class.HasAddSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.HasAddSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.HasAdd where
 
 open import Class.HasAdd.Core public
diff --git a/Class.HasOrder.Core.html b/Class.HasOrder.Core.html
index 61da99b..ec2bfda 100644
--- a/Class.HasOrder.Core.html
+++ b/Class.HasOrder.Core.html
@@ -1,5 +1,5 @@
 
-Class.HasOrder.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.HasOrder.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.HasOrder.Core where
 
 open import Class.Prelude
diff --git a/Class.HasOrder.Instance.html b/Class.HasOrder.Instance.html
index f4937c4..2888c10 100644
--- a/Class.HasOrder.Instance.html
+++ b/Class.HasOrder.Instance.html
@@ -1,5 +1,5 @@
 
-Class.HasOrder.InstanceSource code on Github
{-# OPTIONS --without-K #-}
+Class.HasOrder.InstanceSource code on Github
{-# OPTIONS --without-K #-}
 module Class.HasOrder.Instance where
 
 open import Class.DecEq
diff --git a/Class.HasOrder.html b/Class.HasOrder.html
index 46a984e..3cff8a9 100644
--- a/Class.HasOrder.html
+++ b/Class.HasOrder.html
@@ -1,5 +1,5 @@
 
-Class.HasOrderSource code on Github
module Class.HasOrder where
+Class.HasOrderSource code on Github
module Class.HasOrder where
 
 open import Class.HasOrder.Core public
 open import Class.HasOrder.Instance public
diff --git a/Class.Monad.Core.html b/Class.Monad.Core.html
index 78a4a50..c9bbe1e 100644
--- a/Class.Monad.Core.html
+++ b/Class.Monad.Core.html
@@ -1,5 +1,5 @@
 
-Class.Monad.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Monad.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monad.Core where
 
 open import Class.Prelude
diff --git a/Class.Monad.Instances.html b/Class.Monad.Instances.html
index 13e5044..3da3bb2 100644
--- a/Class.Monad.Instances.html
+++ b/Class.Monad.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Monad.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Monad.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monad.Instances where
 
 open import Class.Prelude
diff --git a/Class.Monad.html b/Class.Monad.html
index fa333fd..ba95e72 100644
--- a/Class.Monad.html
+++ b/Class.Monad.html
@@ -1,5 +1,5 @@
 
-Class.MonadSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.MonadSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monad where
 
 open import Class.Monad.Core public
diff --git a/Class.Monoid.Core.html b/Class.Monoid.Core.html
index ad54f5a..0e999b3 100644
--- a/Class.Monoid.Core.html
+++ b/Class.Monoid.Core.html
@@ -1,5 +1,5 @@
 
-Class.Monoid.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Monoid.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monoid.Core where
 
 open import Class.Prelude
diff --git a/Class.Monoid.Instances.html b/Class.Monoid.Instances.html
index 67525a1..eb62b80 100644
--- a/Class.Monoid.Instances.html
+++ b/Class.Monoid.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Monoid.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Monoid.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monoid.Instances where
 
 open import Class.Prelude
diff --git a/Class.Monoid.html b/Class.Monoid.html
index 3928487..aac93ff 100644
--- a/Class.Monoid.html
+++ b/Class.Monoid.html
@@ -1,5 +1,5 @@
 
-Class.MonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.MonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Monoid where
 
 open import Class.Monoid.Core public
diff --git a/Class.Prelude.html b/Class.Prelude.html
index 6e208d6..5d06049 100644
--- a/Class.Prelude.html
+++ b/Class.Prelude.html
@@ -1,5 +1,5 @@
 
-Class.PreludeSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.PreludeSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Prelude where
 
 open import Agda.Primitive public
diff --git a/Class.Semigroup.Core.html b/Class.Semigroup.Core.html
index beb488d..d4001fa 100644
--- a/Class.Semigroup.Core.html
+++ b/Class.Semigroup.Core.html
@@ -1,5 +1,5 @@
 
-Class.Semigroup.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Semigroup.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Semigroup.Core where
 
 open import Class.Prelude
diff --git a/Class.Semigroup.Instances.html b/Class.Semigroup.Instances.html
index 9bf2d56..fc13ef2 100644
--- a/Class.Semigroup.Instances.html
+++ b/Class.Semigroup.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Semigroup.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Semigroup.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Semigroup.Instances where
 
 open import Class.Prelude
diff --git a/Class.Semigroup.html b/Class.Semigroup.html
index 9f7ed7b..083a9ad 100644
--- a/Class.Semigroup.html
+++ b/Class.Semigroup.html
@@ -1,5 +1,5 @@
 
-Class.SemigroupSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.SemigroupSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Semigroup where
 
 open import Class.Semigroup.Core public
diff --git a/Class.Show.Core.html b/Class.Show.Core.html
index 2d83770..6dada00 100644
--- a/Class.Show.Core.html
+++ b/Class.Show.Core.html
@@ -1,5 +1,5 @@
 
-Class.Show.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Show.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Show.Core where
 
 open import Class.Prelude
diff --git a/Class.Show.Instances.html b/Class.Show.Instances.html
index 12a91ce..1487ab8 100644
--- a/Class.Show.Instances.html
+++ b/Class.Show.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Show.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Show.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Show.Instances where
 
 open import Class.Prelude hiding (Type)
diff --git a/Class.Show.html b/Class.Show.html
index ea14bca..e614f63 100644
--- a/Class.Show.html
+++ b/Class.Show.html
@@ -1,5 +1,5 @@
 
-Class.ShowSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.ShowSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Show where
 
 open import Class.Show.Core public
diff --git a/Class.ToBool.html b/Class.ToBool.html
index ebe1bba..61da933 100644
--- a/Class.ToBool.html
+++ b/Class.ToBool.html
@@ -1,5 +1,5 @@
 
-Class.ToBoolSource code on Github
{-# OPTIONS --without-K #-}
+Class.ToBoolSource code on Github
{-# OPTIONS --without-K #-}
 module Class.ToBool where
 
 open import Class.Prelude hiding (if_then_else_; ⊤; tt)
diff --git a/Class.Traversable.Core.html b/Class.Traversable.Core.html
index ef5d4fb..5d1f44b 100644
--- a/Class.Traversable.Core.html
+++ b/Class.Traversable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Traversable.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Traversable.CoreSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Traversable.Core where
 
 open import Class.Prelude
diff --git a/Class.Traversable.Instances.html b/Class.Traversable.Instances.html
index 7f5d4a3..6d8db1c 100644
--- a/Class.Traversable.Instances.html
+++ b/Class.Traversable.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Traversable.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.Traversable.InstancesSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Traversable.Instances where
 
 open import Class.Prelude
diff --git a/Class.Traversable.html b/Class.Traversable.html
index d83dd89..2a55840 100644
--- a/Class.Traversable.html
+++ b/Class.Traversable.html
@@ -1,5 +1,5 @@
 
-Class.TraversableSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Class.TraversableSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Class.Traversable where
 
 open import Class.Traversable.Core public
diff --git a/Data.Bool.Base.html b/Data.Bool.Base.html
index 347827d..6e56ba2 100644
--- a/Data.Bool.Base.html
+++ b/Data.Bool.Base.html
@@ -1,5 +1,5 @@
 
-Data.Bool.BaseSource code on Github
------------------------------------------------------------------------
+Data.Bool.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The type for booleans and some operations
diff --git a/Data.Bool.Properties.html b/Data.Bool.Properties.html
index 13ada1d..da2ef99 100644
--- a/Data.Bool.Properties.html
+++ b/Data.Bool.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Bool.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Bool.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- A bunch of properties
diff --git a/Data.Bool.Show.html b/Data.Bool.Show.html
index e20f787..2aa936f 100644
--- a/Data.Bool.Show.html
+++ b/Data.Bool.Show.html
@@ -1,5 +1,5 @@
 
-Data.Bool.ShowSource code on Github
------------------------------------------------------------------------
+Data.Bool.ShowSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Showing booleans
diff --git a/Data.Bool.html b/Data.Bool.html
index 5958e63..32b0d0d 100644
--- a/Data.Bool.html
+++ b/Data.Bool.html
@@ -1,5 +1,5 @@
 
-Data.BoolSource code on Github
------------------------------------------------------------------------
+Data.BoolSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Booleans
diff --git a/Data.Char.Base.html b/Data.Char.Base.html
index 25e4099..3354913 100644
--- a/Data.Char.Base.html
+++ b/Data.Char.Base.html
@@ -1,5 +1,5 @@
 
-Data.Char.BaseSource code on Github
------------------------------------------------------------------------
+Data.Char.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic definitions for Characters
diff --git a/Data.Char.Properties.html b/Data.Char.Properties.html
index 3ae6763..b4e5626 100644
--- a/Data.Char.Properties.html
+++ b/Data.Char.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Char.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Char.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of operations on characters
diff --git a/Data.Char.html b/Data.Char.html
index 3b6e8a2..00a4af5 100644
--- a/Data.Char.html
+++ b/Data.Char.html
@@ -1,5 +1,5 @@
 
-Data.CharSource code on Github
------------------------------------------------------------------------
+Data.CharSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Characters
diff --git a/Data.Digit.html b/Data.Digit.html
index 12c11a2..5914fa3 100644
--- a/Data.Digit.html
+++ b/Data.Digit.html
@@ -1,5 +1,5 @@
 
-Data.DigitSource code on Github
------------------------------------------------------------------------
+Data.DigitSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Digits and digit expansions
diff --git a/Data.Empty.Polymorphic.html b/Data.Empty.Polymorphic.html
index 35ec686..7890ef4 100644
--- a/Data.Empty.Polymorphic.html
+++ b/Data.Empty.Polymorphic.html
@@ -1,5 +1,5 @@
 
-Data.Empty.PolymorphicSource code on Github
------------------------------------------------------------------------
+Data.Empty.PolymorphicSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Level polymorphic Empty type
diff --git a/Data.Empty.html b/Data.Empty.html
index ea12c6e..2abecce 100644
--- a/Data.Empty.html
+++ b/Data.Empty.html
@@ -1,5 +1,5 @@
 
-Data.EmptySource code on Github
------------------------------------------------------------------------
+Data.EmptySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Empty type, judgementally proof irrelevant, Level-monomorphic
diff --git a/Data.Fin.Base.html b/Data.Fin.Base.html
index ee2bba8..bd50e35 100644
--- a/Data.Fin.Base.html
+++ b/Data.Fin.Base.html
@@ -1,5 +1,5 @@
 
-Data.Fin.BaseSource code on Github
------------------------------------------------------------------------
+Data.Fin.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Finite sets
diff --git a/Data.Fin.Patterns.html b/Data.Fin.Patterns.html
index 63d6314..56fc6a6 100644
--- a/Data.Fin.Patterns.html
+++ b/Data.Fin.Patterns.html
@@ -1,5 +1,5 @@
 
-Data.Fin.PatternsSource code on Github
------------------------------------------------------------------------
+Data.Fin.PatternsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Patterns for Fin
diff --git a/Data.Fin.Properties.html b/Data.Fin.Properties.html
index 876260a..5e3fcf0 100644
--- a/Data.Fin.Properties.html
+++ b/Data.Fin.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Fin.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Fin.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to Fin, and operations making use of these
diff --git a/Data.Fin.html b/Data.Fin.html
index d3a15cd..1bb39d1 100644
--- a/Data.Fin.html
+++ b/Data.Fin.html
@@ -1,5 +1,5 @@
 
-Data.FinSource code on Github
------------------------------------------------------------------------
+Data.FinSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Finite sets
diff --git a/Data.Float.Base.html b/Data.Float.Base.html
index 0596d0a..4bbde4b 100644
--- a/Data.Float.Base.html
+++ b/Data.Float.Base.html
@@ -1,5 +1,5 @@
 
-Data.Float.BaseSource code on Github
------------------------------------------------------------------------
+Data.Float.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Floats: basic types and operations
diff --git a/Data.Float.Properties.html b/Data.Float.Properties.html
index e94b478..d7b07dd 100644
--- a/Data.Float.Properties.html
+++ b/Data.Float.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Float.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Float.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of operations on floats
diff --git a/Data.Float.html b/Data.Float.html
index b92b4f3..81e0134 100644
--- a/Data.Float.html
+++ b/Data.Float.html
@@ -1,5 +1,5 @@
 
-Data.FloatSource code on Github
------------------------------------------------------------------------
+Data.FloatSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Floating point numbers
diff --git a/Data.Integer.Base.html b/Data.Integer.Base.html
index 9595224..3b0a977 100644
--- a/Data.Integer.Base.html
+++ b/Data.Integer.Base.html
@@ -1,5 +1,5 @@
 
-Data.Integer.BaseSource code on Github
------------------------------------------------------------------------
+Data.Integer.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Integers, basic types and operations
diff --git a/Data.Integer.Coprimality.html b/Data.Integer.Coprimality.html
index 075e014..6c35d15 100644
--- a/Data.Integer.Coprimality.html
+++ b/Data.Integer.Coprimality.html
@@ -1,5 +1,5 @@
 
-Data.Integer.CoprimalitySource code on Github
------------------------------------------------------------------------
+Data.Integer.CoprimalitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Coprimality
diff --git a/Data.Integer.Divisibility.html b/Data.Integer.Divisibility.html
index 78234bb..da34c4a 100644
--- a/Data.Integer.Divisibility.html
+++ b/Data.Integer.Divisibility.html
@@ -1,5 +1,5 @@
 
-Data.Integer.DivisibilitySource code on Github
-----------------------------------------------------------------------
+Data.Integer.DivisibilitySource code on Github
-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Unsigned divisibility
diff --git a/Data.Integer.GCD.html b/Data.Integer.GCD.html
index 7e8f024..0a653cf 100644
--- a/Data.Integer.GCD.html
+++ b/Data.Integer.GCD.html
@@ -1,5 +1,5 @@
 
-Data.Integer.GCDSource code on Github
------------------------------------------------------------------------
+Data.Integer.GCDSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Greatest Common Divisor for integers
diff --git a/Data.Integer.Properties.NatLemmas.html b/Data.Integer.Properties.NatLemmas.html
index 8ac5961..653dff3 100644
--- a/Data.Integer.Properties.NatLemmas.html
+++ b/Data.Integer.Properties.NatLemmas.html
@@ -1,5 +1,5 @@
 
-Data.Integer.Properties.NatLemmasSource code on Github
------------------------------------------------------------------------
+Data.Integer.Properties.NatLemmasSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some extra lemmas about natural numbers only needed for
diff --git a/Data.Integer.Properties.html b/Data.Integer.Properties.html
index 3c9e8d1..2576b70 100644
--- a/Data.Integer.Properties.html
+++ b/Data.Integer.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Integer.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Integer.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some properties about integers
diff --git a/Data.Integer.Show.html b/Data.Integer.Show.html
index 0083524..e1e3936 100644
--- a/Data.Integer.Show.html
+++ b/Data.Integer.Show.html
@@ -1,5 +1,5 @@
 
-Data.Integer.ShowSource code on Github
------------------------------------------------------------------------
+Data.Integer.ShowSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Showing integers
diff --git a/Data.Integer.Solver.html b/Data.Integer.Solver.html
index a585dd1..4c28ea2 100644
--- a/Data.Integer.Solver.html
+++ b/Data.Integer.Solver.html
@@ -1,5 +1,5 @@
 
-Data.Integer.SolverSource code on Github
------------------------------------------------------------------------
+Data.Integer.SolverSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Automatic solvers for equations over integers
diff --git a/Data.Integer.html b/Data.Integer.html
index 3e1cf34..2d08f7c 100644
--- a/Data.Integer.html
+++ b/Data.Integer.html
@@ -1,5 +1,5 @@
 
-Data.IntegerSource code on Github
------------------------------------------------------------------------
+Data.IntegerSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Integers
diff --git a/Data.Irrelevant.html b/Data.Irrelevant.html
index ad8a94e..b260351 100644
--- a/Data.Irrelevant.html
+++ b/Data.Irrelevant.html
@@ -1,5 +1,5 @@
 
-Data.IrrelevantSource code on Github
------------------------------------------------------------------------
+Data.IrrelevantSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Wrapper for the proof irrelevance modality
diff --git a/Data.List.Base.html b/Data.List.Base.html
index cb537a1..00956e1 100644
--- a/Data.List.Base.html
+++ b/Data.List.Base.html
@@ -1,5 +1,5 @@
 
-Data.List.BaseSource code on Github
------------------------------------------------------------------------
+Data.List.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists, basic types and operations
diff --git a/Data.List.Effectful.html b/Data.List.Effectful.html
index 4afd88d..d3fbc9e 100644
--- a/Data.List.Effectful.html
+++ b/Data.List.Effectful.html
@@ -1,5 +1,5 @@
 
-Data.List.EffectfulSource code on Github
------------------------------------------------------------------------
+Data.List.EffectfulSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An effectful view of List
diff --git a/Data.List.Extrema.Core.html b/Data.List.Extrema.Core.html
index 69992a1..eb31572 100644
--- a/Data.List.Extrema.Core.html
+++ b/Data.List.Extrema.Core.html
@@ -1,5 +1,5 @@
 
-Data.List.Extrema.CoreSource code on Github
------------------------------------------------------------------------
+Data.List.Extrema.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core lemmas needed to make list argmin/max functions work
diff --git a/Data.List.Extrema.html b/Data.List.Extrema.html
index e2f4481..658acc5 100644
--- a/Data.List.Extrema.html
+++ b/Data.List.Extrema.html
@@ -1,5 +1,5 @@
 
-Data.List.ExtremaSource code on Github
------------------------------------------------------------------------
+Data.List.ExtremaSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Finding the maximum/minimum values in a list
diff --git a/Data.List.Membership.DecPropositional.html b/Data.List.Membership.DecPropositional.html
index 2e53c5d..31ee78b 100644
--- a/Data.List.Membership.DecPropositional.html
+++ b/Data.List.Membership.DecPropositional.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.DecPropositionalSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.DecPropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Decidable propositional membership over lists
diff --git a/Data.List.Membership.DecSetoid.html b/Data.List.Membership.DecSetoid.html
index fee1d14..10e474e 100644
--- a/Data.List.Membership.DecSetoid.html
+++ b/Data.List.Membership.DecSetoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.DecSetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.DecSetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Decidable setoid membership over lists
diff --git a/Data.List.Membership.Propositional.Properties.Core.html b/Data.List.Membership.Propositional.Properties.Core.html
index 8c0dc5c..7aaaeb9 100644
--- a/Data.List.Membership.Propositional.Properties.Core.html
+++ b/Data.List.Membership.Propositional.Properties.Core.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.Propositional.Properties.CoreSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.Propositional.Properties.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core properties related to propositional list membership.
diff --git a/Data.List.Membership.Propositional.Properties.html b/Data.List.Membership.Propositional.Properties.html
index fd25df9..c77b4f2 100644
--- a/Data.List.Membership.Propositional.Properties.html
+++ b/Data.List.Membership.Propositional.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.Propositional.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.Propositional.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to propositional list membership
diff --git a/Data.List.Membership.Propositional.html b/Data.List.Membership.Propositional.html
index d4b10b5..e000918 100644
--- a/Data.List.Membership.Propositional.html
+++ b/Data.List.Membership.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Data.List.Any.Membership instantiated with propositional equality,
diff --git a/Data.List.Membership.Setoid.Properties.html b/Data.List.Membership.Setoid.Properties.html
index 61082a5..8c21001 100644
--- a/Data.List.Membership.Setoid.Properties.html
+++ b/Data.List.Membership.Setoid.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.Setoid.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.Setoid.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to setoid list membership
diff --git a/Data.List.Membership.Setoid.html b/Data.List.Membership.Setoid.html
index b7a71a9..de8ac68 100644
--- a/Data.List.Membership.Setoid.html
+++ b/Data.List.Membership.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Membership.SetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Membership.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- List membership and some related definitions
diff --git a/Data.List.NonEmpty.Base.html b/Data.List.NonEmpty.Base.html
index 8dddc5b..cac1208 100644
--- a/Data.List.NonEmpty.Base.html
+++ b/Data.List.NonEmpty.Base.html
@@ -1,5 +1,5 @@
 
-Data.List.NonEmpty.BaseSource code on Github
------------------------------------------------------------------------
+Data.List.NonEmpty.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Non-empty lists: base type and operations
diff --git a/Data.List.NonEmpty.html b/Data.List.NonEmpty.html
index ee66369..826e1ed 100644
--- a/Data.List.NonEmpty.html
+++ b/Data.List.NonEmpty.html
@@ -1,5 +1,5 @@
 
-Data.List.NonEmptySource code on Github
------------------------------------------------------------------------
+Data.List.NonEmptySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Non-empty lists
diff --git a/Data.List.Properties.html b/Data.List.Properties.html
index 96849e9..2873188 100644
--- a/Data.List.Properties.html
+++ b/Data.List.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- List-related properties
diff --git a/Data.List.Relation.Binary.Equality.Propositional.html b/Data.List.Relation.Binary.Equality.Propositional.html
index d90535e..fba6a0e 100644
--- a/Data.List.Relation.Binary.Equality.Propositional.html
+++ b/Data.List.Relation.Binary.Equality.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Equality.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Equality.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise equality over lists using propositional equality
diff --git a/Data.List.Relation.Binary.Equality.Setoid.html b/Data.List.Relation.Binary.Equality.Setoid.html
index aef1137..2bfa2b5 100644
--- a/Data.List.Relation.Binary.Equality.Setoid.html
+++ b/Data.List.Relation.Binary.Equality.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Equality.SetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Equality.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise equality over lists parameterised by a setoid
diff --git a/Data.List.Relation.Binary.Lex.Core.html b/Data.List.Relation.Binary.Lex.Core.html
index 84554b6..2a04a4c 100644
--- a/Data.List.Relation.Binary.Lex.Core.html
+++ b/Data.List.Relation.Binary.Lex.Core.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Lex.CoreSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Lex.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lexicographic ordering of lists
diff --git a/Data.List.Relation.Binary.Lex.Strict.html b/Data.List.Relation.Binary.Lex.Strict.html
index a322082..d6060fe 100644
--- a/Data.List.Relation.Binary.Lex.Strict.html
+++ b/Data.List.Relation.Binary.Lex.Strict.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Lex.StrictSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Lex.StrictSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lexicographic ordering of lists
diff --git a/Data.List.Relation.Binary.Lex.html b/Data.List.Relation.Binary.Lex.html
index 76b70f7..226da0d 100644
--- a/Data.List.Relation.Binary.Lex.html
+++ b/Data.List.Relation.Binary.Lex.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.LexSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.LexSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lexicographic ordering of lists
diff --git a/Data.List.Relation.Binary.Pointwise.Base.html b/Data.List.Relation.Binary.Pointwise.Base.html
index 16fae25..7bd4a48 100644
--- a/Data.List.Relation.Binary.Pointwise.Base.html
+++ b/Data.List.Relation.Binary.Pointwise.Base.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Pointwise.BaseSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Pointwise.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise lifting of relations to lists
diff --git a/Data.List.Relation.Binary.Pointwise.Properties.html b/Data.List.Relation.Binary.Pointwise.Properties.html
index 88e898f..727e50e 100644
--- a/Data.List.Relation.Binary.Pointwise.Properties.html
+++ b/Data.List.Relation.Binary.Pointwise.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Pointwise.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Pointwise.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of pointwise lifting of relations to lists
diff --git a/Data.List.Relation.Binary.Pointwise.html b/Data.List.Relation.Binary.Pointwise.html
index 4d0abb1..8fcea4d 100644
--- a/Data.List.Relation.Binary.Pointwise.html
+++ b/Data.List.Relation.Binary.Pointwise.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise lifting of relations to lists
diff --git a/Data.List.Relation.Binary.Subset.Propositional.html b/Data.List.Relation.Binary.Subset.Propositional.html
index cf517a9..a0a2242 100644
--- a/Data.List.Relation.Binary.Subset.Propositional.html
+++ b/Data.List.Relation.Binary.Subset.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Subset.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Subset.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The sublist relation over propositional equality.
diff --git a/Data.List.Relation.Binary.Subset.Setoid.html b/Data.List.Relation.Binary.Subset.Setoid.html
index ceb629c..e7fec0d 100644
--- a/Data.List.Relation.Binary.Subset.Setoid.html
+++ b/Data.List.Relation.Binary.Subset.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Subset.SetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Subset.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The extensional sublist relation over setoid equality.
diff --git a/Data.List.Relation.Unary.All.Properties.html b/Data.List.Relation.Unary.All.Properties.html
index a09324d..1f07bd3 100644
--- a/Data.List.Relation.Unary.All.Properties.html
+++ b/Data.List.Relation.Unary.All.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.All.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.All.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to All
diff --git a/Data.List.Relation.Unary.All.html b/Data.List.Relation.Unary.All.html
index 0e0059a..8ab06e2 100644
--- a/Data.List.Relation.Unary.All.html
+++ b/Data.List.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists where all elements satisfy a given property
diff --git a/Data.List.Relation.Unary.AllPairs.Core.html b/Data.List.Relation.Unary.AllPairs.Core.html
index 237ab3b..404432d 100644
--- a/Data.List.Relation.Unary.AllPairs.Core.html
+++ b/Data.List.Relation.Unary.AllPairs.Core.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.AllPairs.CoreSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.AllPairs.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists where every pair of elements are related (symmetrically)
diff --git a/Data.List.Relation.Unary.AllPairs.html b/Data.List.Relation.Unary.AllPairs.html
index c5b2d8b..5d28014 100644
--- a/Data.List.Relation.Unary.AllPairs.html
+++ b/Data.List.Relation.Unary.AllPairs.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.AllPairsSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.AllPairsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists where every pair of elements are related (symmetrically)
diff --git a/Data.List.Relation.Unary.Any.Properties.html b/Data.List.Relation.Unary.Any.Properties.html
index c32c7a3..161a4ed 100644
--- a/Data.List.Relation.Unary.Any.Properties.html
+++ b/Data.List.Relation.Unary.Any.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.Any.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.Any.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to Any
diff --git a/Data.List.Relation.Unary.Any.html b/Data.List.Relation.Unary.Any.html
index aca35a2..482b63b 100644
--- a/Data.List.Relation.Unary.Any.html
+++ b/Data.List.Relation.Unary.Any.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists where at least one element satisfies a given property
diff --git a/Data.List.Relation.Unary.Unique.Setoid.html b/Data.List.Relation.Unary.Unique.Setoid.html
index 4aae9c2..450bf6d 100644
--- a/Data.List.Relation.Unary.Unique.Setoid.html
+++ b/Data.List.Relation.Unary.Unique.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.Unique.SetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.Unique.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists made up entirely of unique elements (setoid equality)
diff --git a/Data.List.Scans.Base.html b/Data.List.Scans.Base.html
index 1815451..5983306 100644
--- a/Data.List.Scans.Base.html
+++ b/Data.List.Scans.Base.html
@@ -1,5 +1,5 @@
 
-Data.List.Scans.BaseSource code on Github
------------------------------------------------------------------------
+Data.List.Scans.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- List scans: definitions
diff --git a/Data.List.html b/Data.List.html
index 6f2ed19..596f0f1 100644
--- a/Data.List.html
+++ b/Data.List.html
@@ -1,5 +1,5 @@
 
-Data.ListSource code on Github
------------------------------------------------------------------------
+Data.ListSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists
diff --git a/Data.Maybe.Base.html b/Data.Maybe.Base.html
index d1eebc1..a7fd565 100644
--- a/Data.Maybe.Base.html
+++ b/Data.Maybe.Base.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.BaseSource code on Github
------------------------------------------------------------------------
+Data.Maybe.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The Maybe type and some operations
diff --git a/Data.Maybe.Effectful.html b/Data.Maybe.Effectful.html
index 02a9ff9..6e7c228 100644
--- a/Data.Maybe.Effectful.html
+++ b/Data.Maybe.Effectful.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.EffectfulSource code on Github
------------------------------------------------------------------------
+Data.Maybe.EffectfulSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An effectful view of Maybe
diff --git a/Data.Maybe.Properties.html b/Data.Maybe.Properties.html
index 14938d3..9097168 100644
--- a/Data.Maybe.Properties.html
+++ b/Data.Maybe.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Maybe.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Maybe-related properties
diff --git a/Data.Maybe.Relation.Unary.All.html b/Data.Maybe.Relation.Unary.All.html
index ee8be33..76f7a58 100644
--- a/Data.Maybe.Relation.Unary.All.html
+++ b/Data.Maybe.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.Maybe.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Maybes where all the elements satisfy a given property
diff --git a/Data.Maybe.Relation.Unary.Any.html b/Data.Maybe.Relation.Unary.Any.html
index 10dbe83..15b19a0 100644
--- a/Data.Maybe.Relation.Unary.Any.html
+++ b/Data.Maybe.Relation.Unary.Any.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
+Data.Maybe.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Maybes where one of the elements satisfies a given property
diff --git a/Data.Maybe.html b/Data.Maybe.html
index f3e36cc..31f7009 100644
--- a/Data.Maybe.html
+++ b/Data.Maybe.html
@@ -1,5 +1,5 @@
 
-Data.MaybeSource code on Github
------------------------------------------------------------------------
+Data.MaybeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The Maybe type
diff --git a/Data.Nat.Base.html b/Data.Nat.Base.html
index 7bf26e8..c0669f8 100644
--- a/Data.Nat.Base.html
+++ b/Data.Nat.Base.html
@@ -1,5 +1,5 @@
 
-Data.Nat.BaseSource code on Github
------------------------------------------------------------------------
+Data.Nat.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Natural numbers, basic types and operations
diff --git a/Data.Nat.Binary.Base.html b/Data.Nat.Binary.Base.html
index c052f27..9dbc8ee 100644
--- a/Data.Nat.Binary.Base.html
+++ b/Data.Nat.Binary.Base.html
@@ -1,5 +1,5 @@
 
-Data.Nat.Binary.BaseSource code on Github
------------------------------------------------------------------------
+Data.Nat.Binary.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Natural numbers represented in binary.
diff --git a/Data.Nat.Binary.Properties.html b/Data.Nat.Binary.Properties.html
index 3ce5c7d..9b96ad6 100644
--- a/Data.Nat.Binary.Properties.html
+++ b/Data.Nat.Binary.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Nat.Binary.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Nat.Binary.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic properties of ℕᵇ
diff --git a/Data.Nat.Binary.html b/Data.Nat.Binary.html
index 2f05578..e0e5443 100644
--- a/Data.Nat.Binary.html
+++ b/Data.Nat.Binary.html
@@ -1,5 +1,5 @@
 
-Data.Nat.BinarySource code on Github
------------------------------------------------------------------------
+Data.Nat.BinarySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Natural numbers represented in binary natively in Agda.
diff --git a/Data.Nat.Coprimality.html b/Data.Nat.Coprimality.html
index cb90f18..4adfcae 100644
--- a/Data.Nat.Coprimality.html
+++ b/Data.Nat.Coprimality.html
@@ -1,5 +1,5 @@
 
-Data.Nat.CoprimalitySource code on Github
------------------------------------------------------------------------
+Data.Nat.CoprimalitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Coprimality
diff --git a/Data.Nat.DivMod.Core.html b/Data.Nat.DivMod.Core.html
index 7f871c0..d355a17 100644
--- a/Data.Nat.DivMod.Core.html
+++ b/Data.Nat.DivMod.Core.html
@@ -1,5 +1,5 @@
 
-Data.Nat.DivMod.CoreSource code on Github
------------------------------------------------------------------------
+Data.Nat.DivMod.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core lemmas for division and modulus operations
diff --git a/Data.Nat.DivMod.html b/Data.Nat.DivMod.html
index 0354040..74936bc 100644
--- a/Data.Nat.DivMod.html
+++ b/Data.Nat.DivMod.html
@@ -1,5 +1,5 @@
 
-Data.Nat.DivModSource code on Github
------------------------------------------------------------------------
+Data.Nat.DivModSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Natural number division
diff --git a/Data.Nat.Divisibility.Core.html b/Data.Nat.Divisibility.Core.html
index 3c00e36..7199b15 100644
--- a/Data.Nat.Divisibility.Core.html
+++ b/Data.Nat.Divisibility.Core.html
@@ -1,5 +1,5 @@
 
-Data.Nat.Divisibility.CoreSource code on Github
------------------------------------------------------------------------
+Data.Nat.Divisibility.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core definition of divisibility
diff --git a/Data.Nat.Divisibility.html b/Data.Nat.Divisibility.html
index 41630a5..f085451 100644
--- a/Data.Nat.Divisibility.html
+++ b/Data.Nat.Divisibility.html
@@ -1,5 +1,5 @@
 
-Data.Nat.DivisibilitySource code on Github
------------------------------------------------------------------------
+Data.Nat.DivisibilitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Divisibility
diff --git a/Data.Nat.GCD.Lemmas.html b/Data.Nat.GCD.Lemmas.html
index 4de8552..5fa7c2d 100644
--- a/Data.Nat.GCD.Lemmas.html
+++ b/Data.Nat.GCD.Lemmas.html
@@ -1,5 +1,5 @@
 
-Data.Nat.GCD.LemmasSource code on Github
------------------------------------------------------------------------
+Data.Nat.GCD.LemmasSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
diff --git a/Data.Nat.GCD.html b/Data.Nat.GCD.html
index 4cbe561..a824f67 100644
--- a/Data.Nat.GCD.html
+++ b/Data.Nat.GCD.html
@@ -1,5 +1,5 @@
 
-Data.Nat.GCDSource code on Github
------------------------------------------------------------------------
+Data.Nat.GCDSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Greatest common divisor
diff --git a/Data.Nat.GeneralisedArithmetic.html b/Data.Nat.GeneralisedArithmetic.html
index ffb9a89..1093dc4 100644
--- a/Data.Nat.GeneralisedArithmetic.html
+++ b/Data.Nat.GeneralisedArithmetic.html
@@ -1,5 +1,5 @@
 
-Data.Nat.GeneralisedArithmeticSource code on Github
------------------------------------------------------------------------
+Data.Nat.GeneralisedArithmeticSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- A generalisation of the arithmetic operations
diff --git a/Data.Nat.Induction.html b/Data.Nat.Induction.html
index 89a7875..0b5179f 100644
--- a/Data.Nat.Induction.html
+++ b/Data.Nat.Induction.html
@@ -1,5 +1,5 @@
 
-Data.Nat.InductionSource code on Github
------------------------------------------------------------------------
+Data.Nat.InductionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Various forms of induction for natural numbers
diff --git a/Data.Nat.Primality.html b/Data.Nat.Primality.html
index 9789fcb..65a2a98 100644
--- a/Data.Nat.Primality.html
+++ b/Data.Nat.Primality.html
@@ -1,5 +1,5 @@
 
-Data.Nat.PrimalitySource code on Github
------------------------------------------------------------------------
+Data.Nat.PrimalitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Primality
diff --git a/Data.Nat.Properties.html b/Data.Nat.Properties.html
index 120f8a9..c29ed19 100644
--- a/Data.Nat.Properties.html
+++ b/Data.Nat.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Nat.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Nat.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- A bunch of properties about natural number operations
diff --git a/Data.Nat.Show.html b/Data.Nat.Show.html
index ebc4c7b..f65eec8 100644
--- a/Data.Nat.Show.html
+++ b/Data.Nat.Show.html
@@ -1,5 +1,5 @@
 
-Data.Nat.ShowSource code on Github
------------------------------------------------------------------------
+Data.Nat.ShowSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Showing natural numbers
diff --git a/Data.Nat.Solver.html b/Data.Nat.Solver.html
index 031cc7f..67aff20 100644
--- a/Data.Nat.Solver.html
+++ b/Data.Nat.Solver.html
@@ -1,5 +1,5 @@
 
-Data.Nat.SolverSource code on Github
------------------------------------------------------------------------
+Data.Nat.SolverSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Automatic solvers for equations over naturals
diff --git a/Data.Nat.html b/Data.Nat.html
index d386d62..ba9ed3c 100644
--- a/Data.Nat.html
+++ b/Data.Nat.html
@@ -1,5 +1,5 @@
 
-Data.NatSource code on Github
------------------------------------------------------------------------
+Data.NatSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Natural numbers
diff --git a/Data.Parity.Base.html b/Data.Parity.Base.html
index 323f6f9..05668f7 100644
--- a/Data.Parity.Base.html
+++ b/Data.Parity.Base.html
@@ -1,5 +1,5 @@
 
-Data.Parity.BaseSource code on Github
------------------------------------------------------------------------
+Data.Parity.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Parity
diff --git a/Data.Product.Algebra.html b/Data.Product.Algebra.html
index 51cd5ae..6c35ca7 100644
--- a/Data.Product.Algebra.html
+++ b/Data.Product.Algebra.html
@@ -1,5 +1,5 @@
 
-Data.Product.AlgebraSource code on Github
------------------------------------------------------------------------
+Data.Product.AlgebraSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Algebraic properties of products
diff --git a/Data.Product.Base.html b/Data.Product.Base.html
index 3f77984..f5de3f3 100644
--- a/Data.Product.Base.html
+++ b/Data.Product.Base.html
@@ -1,5 +1,5 @@
 
-Data.Product.BaseSource code on Github
------------------------------------------------------------------------
+Data.Product.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Products
diff --git a/Data.Product.Function.Dependent.Propositional.html b/Data.Product.Function.Dependent.Propositional.html
index 2620cb9..ae188f3 100644
--- a/Data.Product.Function.Dependent.Propositional.html
+++ b/Data.Product.Function.Dependent.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.Product.Function.Dependent.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.Product.Function.Dependent.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Dependent product combinators for propositional equality
diff --git a/Data.Product.Function.NonDependent.Propositional.html b/Data.Product.Function.NonDependent.Propositional.html
index da4f8fc..de208ce 100644
--- a/Data.Product.Function.NonDependent.Propositional.html
+++ b/Data.Product.Function.NonDependent.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.Product.Function.NonDependent.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.Product.Function.NonDependent.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Non-dependent product combinators for propositional equality
diff --git a/Data.Product.Function.NonDependent.Setoid.html b/Data.Product.Function.NonDependent.Setoid.html
index a7093d1..6bf2326 100644
--- a/Data.Product.Function.NonDependent.Setoid.html
+++ b/Data.Product.Function.NonDependent.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.Product.Function.NonDependent.SetoidSource code on Github
------------------------------------------------------------------------
+Data.Product.Function.NonDependent.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Non-dependent product combinators for setoid equality preserving
diff --git a/Data.Product.Nary.NonDependent.html b/Data.Product.Nary.NonDependent.html
index 20b372c..9628ac1 100644
--- a/Data.Product.Nary.NonDependent.html
+++ b/Data.Product.Nary.NonDependent.html
@@ -1,5 +1,5 @@
 
-Data.Product.Nary.NonDependentSource code on Github
------------------------------------------------------------------------
+Data.Product.Nary.NonDependentSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Nondependent heterogeneous N-ary products
diff --git a/Data.Product.Properties.html b/Data.Product.Properties.html
index 71ad092..a470fcf 100644
--- a/Data.Product.Properties.html
+++ b/Data.Product.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Product.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Product.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of products
diff --git a/Data.Product.Relation.Binary.Pointwise.NonDependent.html b/Data.Product.Relation.Binary.Pointwise.NonDependent.html
index d5850bd..992ae17 100644
--- a/Data.Product.Relation.Binary.Pointwise.NonDependent.html
+++ b/Data.Product.Relation.Binary.Pointwise.NonDependent.html
@@ -1,5 +1,5 @@
 
-Data.Product.Relation.Binary.Pointwise.NonDependentSource code on Github
------------------------------------------------------------------------
+Data.Product.Relation.Binary.Pointwise.NonDependentSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise products of binary relations
diff --git a/Data.Product.Relation.Unary.All.html b/Data.Product.Relation.Unary.All.html
index 80eb7fd..a91da83 100644
--- a/Data.Product.Relation.Unary.All.html
+++ b/Data.Product.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.Product.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.Product.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lifting of two predicates
diff --git a/Data.Product.html b/Data.Product.html
index 6da6b62..2dee240 100644
--- a/Data.Product.html
+++ b/Data.Product.html
@@ -1,5 +1,5 @@
 
-Data.ProductSource code on Github
------------------------------------------------------------------------
+Data.ProductSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Products
diff --git a/Data.Rational.Base.html b/Data.Rational.Base.html
index 7382175..e921b24 100644
--- a/Data.Rational.Base.html
+++ b/Data.Rational.Base.html
@@ -1,5 +1,5 @@
 
-Data.Rational.BaseSource code on Github
------------------------------------------------------------------------
+Data.Rational.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Rational numbers
diff --git a/Data.Rational.Properties.html b/Data.Rational.Properties.html
index da2b202..c10a4dc 100644
--- a/Data.Rational.Properties.html
+++ b/Data.Rational.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Rational.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Rational.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of Rational numbers
diff --git a/Data.Rational.Unnormalised.Base.html b/Data.Rational.Unnormalised.Base.html
index 4a1230d..f565fbf 100644
--- a/Data.Rational.Unnormalised.Base.html
+++ b/Data.Rational.Unnormalised.Base.html
@@ -1,5 +1,5 @@
 
-Data.Rational.Unnormalised.BaseSource code on Github
------------------------------------------------------------------------
+Data.Rational.Unnormalised.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Rational numbers in non-reduced form.
diff --git a/Data.Rational.Unnormalised.Properties.html b/Data.Rational.Unnormalised.Properties.html
index ac7087f..ac96f71 100644
--- a/Data.Rational.Unnormalised.Properties.html
+++ b/Data.Rational.Unnormalised.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Rational.Unnormalised.PropertiesSource code on Github
-----------------------------------------------------------------------
+Data.Rational.Unnormalised.PropertiesSource code on Github
-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of unnormalized Rational numbers
diff --git a/Data.Rational.html b/Data.Rational.html
index d4801ec..a27add9 100644
--- a/Data.Rational.html
+++ b/Data.Rational.html
@@ -1,5 +1,5 @@
 
-Data.RationalSource code on Github
------------------------------------------------------------------------
+Data.RationalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Rational numbers
diff --git a/Data.Sign.Base.html b/Data.Sign.Base.html
index 44312c5..fd535e0 100644
--- a/Data.Sign.Base.html
+++ b/Data.Sign.Base.html
@@ -1,5 +1,5 @@
 
-Data.Sign.BaseSource code on Github
------------------------------------------------------------------------
+Data.Sign.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Signs
diff --git a/Data.Sign.Properties.html b/Data.Sign.Properties.html
index 7fa3897..af07a38 100644
--- a/Data.Sign.Properties.html
+++ b/Data.Sign.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Sign.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Sign.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some properties about signs
diff --git a/Data.Sign.html b/Data.Sign.html
index a2482fe..50d9101 100644
--- a/Data.Sign.html
+++ b/Data.Sign.html
@@ -1,5 +1,5 @@
 
-Data.SignSource code on Github
------------------------------------------------------------------------
+Data.SignSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Signs
diff --git a/Data.String.Base.html b/Data.String.Base.html
index d7aa1ed..ba23f90 100644
--- a/Data.String.Base.html
+++ b/Data.String.Base.html
@@ -1,5 +1,5 @@
 
-Data.String.BaseSource code on Github
------------------------------------------------------------------------
+Data.String.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Strings: builtin type and basic operations
diff --git a/Data.String.Properties.html b/Data.String.Properties.html
index ae7e5f4..3f1143a 100644
--- a/Data.String.Properties.html
+++ b/Data.String.Properties.html
@@ -1,5 +1,5 @@
 
-Data.String.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.String.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of operations on strings
diff --git a/Data.String.html b/Data.String.html
index 742fbf6..617776b 100644
--- a/Data.String.html
+++ b/Data.String.html
@@ -1,5 +1,5 @@
 
-Data.StringSource code on Github
------------------------------------------------------------------------
+Data.StringSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Strings
diff --git a/Data.Sum.Algebra.html b/Data.Sum.Algebra.html
index 26ed53c..2b3eda0 100644
--- a/Data.Sum.Algebra.html
+++ b/Data.Sum.Algebra.html
@@ -1,5 +1,5 @@
 
-Data.Sum.AlgebraSource code on Github
------------------------------------------------------------------------
+Data.Sum.AlgebraSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Algebraic properties of sums (disjoint unions)
diff --git a/Data.Sum.Base.html b/Data.Sum.Base.html
index ce7e967..3110c73 100644
--- a/Data.Sum.Base.html
+++ b/Data.Sum.Base.html
@@ -1,5 +1,5 @@
 
-Data.Sum.BaseSource code on Github
------------------------------------------------------------------------
+Data.Sum.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sums (disjoint unions)
diff --git a/Data.Sum.Effectful.Left.html b/Data.Sum.Effectful.Left.html
index cd7e6a7..5762539 100644
--- a/Data.Sum.Effectful.Left.html
+++ b/Data.Sum.Effectful.Left.html
@@ -1,5 +1,5 @@
 
-Data.Sum.Effectful.LeftSource code on Github
------------------------------------------------------------------------
+Data.Sum.Effectful.LeftSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An effectful view of the Sum type (Left-biased)
diff --git a/Data.Sum.Function.Propositional.html b/Data.Sum.Function.Propositional.html
index e18a1e6..45f94b2 100644
--- a/Data.Sum.Function.Propositional.html
+++ b/Data.Sum.Function.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.Sum.Function.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.Sum.Function.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sum combinators for propositional equality preserving functions
diff --git a/Data.Sum.Function.Setoid.html b/Data.Sum.Function.Setoid.html
index cf5da2d..5584660 100644
--- a/Data.Sum.Function.Setoid.html
+++ b/Data.Sum.Function.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.Sum.Function.SetoidSource code on Github
------------------------------------------------------------------------
+Data.Sum.Function.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sum combinators for setoid equality preserving functions
diff --git a/Data.Sum.Properties.html b/Data.Sum.Properties.html
index b37c398..8d81438 100644
--- a/Data.Sum.Properties.html
+++ b/Data.Sum.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Sum.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Sum.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of sums (disjoint unions)
diff --git a/Data.Sum.Relation.Binary.Pointwise.html b/Data.Sum.Relation.Binary.Pointwise.html
index 1b3ab8e..78890f2 100644
--- a/Data.Sum.Relation.Binary.Pointwise.html
+++ b/Data.Sum.Relation.Binary.Pointwise.html
@@ -1,5 +1,5 @@
 
-Data.Sum.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
+Data.Sum.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise sum
diff --git a/Data.Sum.Relation.Unary.All.html b/Data.Sum.Relation.Unary.All.html
index a095dbd..8c8ca43 100644
--- a/Data.Sum.Relation.Unary.All.html
+++ b/Data.Sum.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.Sum.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.Sum.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Heterogeneous `All` predicate for disjoint sums
diff --git a/Data.Sum.html b/Data.Sum.html
index 212384c..78af0d5 100644
--- a/Data.Sum.html
+++ b/Data.Sum.html
@@ -1,5 +1,5 @@
 
-Data.SumSource code on Github
------------------------------------------------------------------------
+Data.SumSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sums (disjoint unions)
diff --git a/Data.These.Base.html b/Data.These.Base.html
index b0b62fa..45c8aad 100644
--- a/Data.These.Base.html
+++ b/Data.These.Base.html
@@ -1,5 +1,5 @@
 
-Data.These.BaseSource code on Github
------------------------------------------------------------------------
+Data.These.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An either-or-both data type, basic type and operations
diff --git a/Data.These.Properties.html b/Data.These.Properties.html
index 67fc036..55342e1 100644
--- a/Data.These.Properties.html
+++ b/Data.These.Properties.html
@@ -1,5 +1,5 @@
 
-Data.These.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.These.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of These
diff --git a/Data.These.html b/Data.These.html
index 49030c1..5d44972 100644
--- a/Data.These.html
+++ b/Data.These.html
@@ -1,5 +1,5 @@
 
-Data.TheseSource code on Github
------------------------------------------------------------------------
+Data.TheseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An either-or-both data type
diff --git a/Data.Unit.Base.html b/Data.Unit.Base.html
index a3084c5..aa1f7e6 100644
--- a/Data.Unit.Base.html
+++ b/Data.Unit.Base.html
@@ -1,5 +1,5 @@
 
-Data.Unit.BaseSource code on Github
------------------------------------------------------------------------
+Data.Unit.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The unit type and the total relation on unit
diff --git a/Data.Unit.Polymorphic.Base.html b/Data.Unit.Polymorphic.Base.html
index 80e4ae3..7d7916c 100644
--- a/Data.Unit.Polymorphic.Base.html
+++ b/Data.Unit.Polymorphic.Base.html
@@ -1,5 +1,5 @@
 
-Data.Unit.Polymorphic.BaseSource code on Github
------------------------------------------------------------------------
+Data.Unit.Polymorphic.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- A universe polymorphic unit type, as a Lift of the Level 0 one.
diff --git a/Data.Unit.Polymorphic.Properties.html b/Data.Unit.Polymorphic.Properties.html
index 33f0381..ba46aff 100644
--- a/Data.Unit.Polymorphic.Properties.html
+++ b/Data.Unit.Polymorphic.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Unit.Polymorphic.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Unit.Polymorphic.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of the polymorphic unit type
diff --git a/Data.Unit.Polymorphic.html b/Data.Unit.Polymorphic.html
index 97709d7..819545e 100644
--- a/Data.Unit.Polymorphic.html
+++ b/Data.Unit.Polymorphic.html
@@ -1,5 +1,5 @@
 
-Data.Unit.PolymorphicSource code on Github
------------------------------------------------------------------------
+Data.Unit.PolymorphicSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The universe polymorphic unit type and the total relation on unit
diff --git a/Data.Unit.Properties.html b/Data.Unit.Properties.html
index 258625d..bacc29e 100644
--- a/Data.Unit.Properties.html
+++ b/Data.Unit.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Unit.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Unit.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of the unit type
diff --git a/Data.Unit.html b/Data.Unit.html
index ad18c54..c273409 100644
--- a/Data.Unit.html
+++ b/Data.Unit.html
@@ -1,5 +1,5 @@
 
-Data.UnitSource code on Github
------------------------------------------------------------------------
+Data.UnitSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The unit type, Level-monomorphic version
diff --git a/Data.Vec.Base.html b/Data.Vec.Base.html
index 855ae6e..782ed1d 100644
--- a/Data.Vec.Base.html
+++ b/Data.Vec.Base.html
@@ -1,5 +1,5 @@
 
-Data.Vec.BaseSource code on Github
------------------------------------------------------------------------
+Data.Vec.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Vectors, basic types and operations
diff --git a/Data.Vec.Bounded.Base.html b/Data.Vec.Bounded.Base.html
index 3fdcd0a..47d7b53 100644
--- a/Data.Vec.Bounded.Base.html
+++ b/Data.Vec.Bounded.Base.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Bounded.BaseSource code on Github
------------------------------------------------------------------------
+Data.Vec.Bounded.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bounded vectors, basic types and operations
diff --git a/Data.Vec.Functional.html b/Data.Vec.Functional.html
index 6f43e2a..17108e2 100644
--- a/Data.Vec.Functional.html
+++ b/Data.Vec.Functional.html
@@ -1,5 +1,5 @@
 
-Data.Vec.FunctionalSource code on Github
------------------------------------------------------------------------
+Data.Vec.FunctionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Vectors defined as functions from a finite set to a type.
diff --git a/Data.Vec.Membership.Propositional.html b/Data.Vec.Membership.Propositional.html
index 731ad36..abf3835 100644
--- a/Data.Vec.Membership.Propositional.html
+++ b/Data.Vec.Membership.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Membership.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.Vec.Membership.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Data.Vec.Any.Membership instantiated with propositional equality,
diff --git a/Data.Vec.Membership.Setoid.html b/Data.Vec.Membership.Setoid.html
index 216fd6d..0a175c5 100644
--- a/Data.Vec.Membership.Setoid.html
+++ b/Data.Vec.Membership.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Membership.SetoidSource code on Github
------------------------------------------------------------------------
+Data.Vec.Membership.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Membership of vectors, along with some additional definitions.
diff --git a/Data.Vec.N-ary.html b/Data.Vec.N-ary.html
index 3b9b8f9..d3c2eae 100644
--- a/Data.Vec.N-ary.html
+++ b/Data.Vec.N-ary.html
@@ -1,5 +1,5 @@
 
-Data.Vec.N-arySource code on Github
------------------------------------------------------------------------
+Data.Vec.N-arySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Code for converting Vec A n → B to and from n-ary functions
diff --git a/Data.Vec.Properties.html b/Data.Vec.Properties.html
index d4de002..de949a5 100644
--- a/Data.Vec.Properties.html
+++ b/Data.Vec.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Vec.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Vec.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some Vec-related properties
diff --git a/Data.Vec.Relation.Binary.Equality.Cast.html b/Data.Vec.Relation.Binary.Equality.Cast.html
index f6f43ff..a85e272 100644
--- a/Data.Vec.Relation.Binary.Equality.Cast.html
+++ b/Data.Vec.Relation.Binary.Equality.Cast.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Relation.Binary.Equality.CastSource code on Github
------------------------------------------------------------------------
+Data.Vec.Relation.Binary.Equality.CastSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An equational reasoning library for propositional equality over
diff --git a/Data.Vec.Relation.Unary.All.html b/Data.Vec.Relation.Unary.All.html
index a837045..a708af4 100644
--- a/Data.Vec.Relation.Unary.All.html
+++ b/Data.Vec.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.Vec.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Vectors where all elements satisfy a given property
diff --git a/Data.Vec.Relation.Unary.Any.html b/Data.Vec.Relation.Unary.Any.html
index 199eeb8..d1b4eaf 100644
--- a/Data.Vec.Relation.Unary.Any.html
+++ b/Data.Vec.Relation.Unary.Any.html
@@ -1,5 +1,5 @@
 
-Data.Vec.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
+Data.Vec.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Vectors where at least one element satisfies a given property
diff --git a/Data.Vec.html b/Data.Vec.html
index 0b130c2..e01e013 100644
--- a/Data.Vec.html
+++ b/Data.Vec.html
@@ -1,5 +1,5 @@
 
-Data.VecSource code on Github
------------------------------------------------------------------------
+Data.VecSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Vectors
diff --git a/Data.Word64.Base.html b/Data.Word64.Base.html
index 544b4a8..b79ffca 100644
--- a/Data.Word64.Base.html
+++ b/Data.Word64.Base.html
@@ -1,5 +1,5 @@
 
-Data.Word64.BaseSource code on Github
------------------------------------------------------------------------
+Data.Word64.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Machine words: basic type and conversion functions
diff --git a/Data.Word64.Properties.html b/Data.Word64.Properties.html
index 5b86ccf..fe610d1 100644
--- a/Data.Word64.Properties.html
+++ b/Data.Word64.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Word64.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Word64.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of operations on machine words
diff --git a/Effect.Applicative.html b/Effect.Applicative.html
index 975a192..a22824b 100644
--- a/Effect.Applicative.html
+++ b/Effect.Applicative.html
@@ -1,5 +1,5 @@
 
-Effect.ApplicativeSource code on Github
------------------------------------------------------------------------
+Effect.ApplicativeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Applicative functors
diff --git a/Effect.Choice.html b/Effect.Choice.html
index 73fa9ed..39b88b0 100644
--- a/Effect.Choice.html
+++ b/Effect.Choice.html
@@ -1,5 +1,5 @@
 
-Effect.ChoiceSource code on Github
------------------------------------------------------------------------
+Effect.ChoiceSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Type constructors giving rise to a semigroup at every type
diff --git a/Effect.Empty.html b/Effect.Empty.html
index 167b0cd..ea94024 100644
--- a/Effect.Empty.html
+++ b/Effect.Empty.html
@@ -1,5 +1,5 @@
 
-Effect.EmptySource code on Github
------------------------------------------------------------------------
+Effect.EmptySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Empty values (e.g. [] for List, nothing for Maybe)
diff --git a/Effect.Functor.html b/Effect.Functor.html
index 4235c4a..b825c0c 100644
--- a/Effect.Functor.html
+++ b/Effect.Functor.html
@@ -1,5 +1,5 @@
 
-Effect.FunctorSource code on Github
------------------------------------------------------------------------
+Effect.FunctorSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Functors
diff --git a/Effect.Monad.html b/Effect.Monad.html
index e2dae63..4582b7e 100644
--- a/Effect.Monad.html
+++ b/Effect.Monad.html
@@ -1,5 +1,5 @@
 
-Effect.MonadSource code on Github
------------------------------------------------------------------------
+Effect.MonadSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Monads
diff --git a/Function.Base.html b/Function.Base.html
index c53feb2..95b878d 100644
--- a/Function.Base.html
+++ b/Function.Base.html
@@ -1,5 +1,5 @@
 
-Function.BaseSource code on Github
------------------------------------------------------------------------
+Function.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Simple combinators working solely on and with functions
diff --git a/Function.Bundles.html b/Function.Bundles.html
index ed19142..444f9ba 100644
--- a/Function.Bundles.html
+++ b/Function.Bundles.html
@@ -1,5 +1,5 @@
 
-Function.BundlesSource code on Github
------------------------------------------------------------------------
+Function.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for types of functions
diff --git a/Function.Consequences.Propositional.html b/Function.Consequences.Propositional.html
index 9bdd11d..77c42ba 100644
--- a/Function.Consequences.Propositional.html
+++ b/Function.Consequences.Propositional.html
@@ -1,5 +1,5 @@
 
-Function.Consequences.PropositionalSource code on Github
------------------------------------------------------------------------
+Function.Consequences.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relationships between properties of functions where the equality
diff --git a/Function.Consequences.Setoid.html b/Function.Consequences.Setoid.html
index 9951059..76da075 100644
--- a/Function.Consequences.Setoid.html
+++ b/Function.Consequences.Setoid.html
@@ -1,5 +1,5 @@
 
-Function.Consequences.SetoidSource code on Github
------------------------------------------------------------------------
+Function.Consequences.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relationships between properties of functions where the equality
diff --git a/Function.Consequences.html b/Function.Consequences.html
index b20f33a..d260252 100644
--- a/Function.Consequences.html
+++ b/Function.Consequences.html
@@ -1,5 +1,5 @@
 
-Function.ConsequencesSource code on Github
------------------------------------------------------------------------
+Function.ConsequencesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relationships between properties of functions. See
diff --git a/Function.Construct.Composition.html b/Function.Construct.Composition.html
index 487ebbf..0df187f 100644
--- a/Function.Construct.Composition.html
+++ b/Function.Construct.Composition.html
@@ -1,5 +1,5 @@
 
-Function.Construct.CompositionSource code on Github
------------------------------------------------------------------------
+Function.Construct.CompositionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Composition of functional properties
diff --git a/Function.Construct.Identity.html b/Function.Construct.Identity.html
index 0c3b6f5..a622c0d 100644
--- a/Function.Construct.Identity.html
+++ b/Function.Construct.Identity.html
@@ -1,5 +1,5 @@
 
-Function.Construct.IdentitySource code on Github
------------------------------------------------------------------------
+Function.Construct.IdentitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The identity function
diff --git a/Function.Construct.Symmetry.html b/Function.Construct.Symmetry.html
index 3ab2e2c..cbec817 100644
--- a/Function.Construct.Symmetry.html
+++ b/Function.Construct.Symmetry.html
@@ -1,5 +1,5 @@
 
-Function.Construct.SymmetrySource code on Github
------------------------------------------------------------------------
+Function.Construct.SymmetrySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some functional properties are symmetric
diff --git a/Function.Core.html b/Function.Core.html
index 7009660..d6299bb 100644
--- a/Function.Core.html
+++ b/Function.Core.html
@@ -1,5 +1,5 @@
 
-Function.CoreSource code on Github
------------------------------------------------------------------------
+Function.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core definitions for Functions
diff --git a/Function.Definitions.html b/Function.Definitions.html
index fa248e4..e72be8b 100644
--- a/Function.Definitions.html
+++ b/Function.Definitions.html
@@ -1,5 +1,5 @@
 
-Function.DefinitionsSource code on Github
------------------------------------------------------------------------
+Function.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions for types of functions.
diff --git a/Function.Dependent.Bundles.html b/Function.Dependent.Bundles.html
index c8ebe13..ed875e4 100644
--- a/Function.Dependent.Bundles.html
+++ b/Function.Dependent.Bundles.html
@@ -1,5 +1,5 @@
 
-Function.Dependent.BundlesSource code on Github
------------------------------------------------------------------------
+Function.Dependent.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for types of functions
diff --git a/Function.Indexed.Relation.Binary.Equality.html b/Function.Indexed.Relation.Binary.Equality.html
index a5f261b..a28142c 100644
--- a/Function.Indexed.Relation.Binary.Equality.html
+++ b/Function.Indexed.Relation.Binary.Equality.html
@@ -1,5 +1,5 @@
 
-Function.Indexed.Relation.Binary.EqualitySource code on Github
------------------------------------------------------------------------
+Function.Indexed.Relation.Binary.EqualitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Function setoids and related constructions
diff --git a/Function.Metric.Bundles.html b/Function.Metric.Bundles.html
index 56c06f8..141701d 100644
--- a/Function.Metric.Bundles.html
+++ b/Function.Metric.Bundles.html
@@ -1,5 +1,5 @@
 
-Function.Metric.BundlesSource code on Github
------------------------------------------------------------------------
+Function.Metric.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for metrics
diff --git a/Function.Metric.Core.html b/Function.Metric.Core.html
index e8e2b26..73b7bf2 100644
--- a/Function.Metric.Core.html
+++ b/Function.Metric.Core.html
@@ -1,5 +1,5 @@
 
-Function.Metric.CoreSource code on Github
------------------------------------------------------------------------
+Function.Metric.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core metric definitions
diff --git a/Function.Metric.Definitions.html b/Function.Metric.Definitions.html
index 0ec6378..ed6a336 100644
--- a/Function.Metric.Definitions.html
+++ b/Function.Metric.Definitions.html
@@ -1,5 +1,5 @@
 
-Function.Metric.DefinitionsSource code on Github
------------------------------------------------------------------------
+Function.Metric.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions of properties over distance functions
diff --git a/Function.Metric.Nat.Bundles.html b/Function.Metric.Nat.Bundles.html
index 458670c..945b1d5 100644
--- a/Function.Metric.Nat.Bundles.html
+++ b/Function.Metric.Nat.Bundles.html
@@ -1,5 +1,5 @@
 
-Function.Metric.Nat.BundlesSource code on Github
------------------------------------------------------------------------
+Function.Metric.Nat.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for metrics over â„•
diff --git a/Function.Metric.Nat.Core.html b/Function.Metric.Nat.Core.html
index 1c9194d..7eee405 100644
--- a/Function.Metric.Nat.Core.html
+++ b/Function.Metric.Nat.Core.html
@@ -1,5 +1,5 @@
 
-Function.Metric.Nat.CoreSource code on Github
------------------------------------------------------------------------
+Function.Metric.Nat.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core definitions for metrics over â„•
diff --git a/Function.Metric.Nat.Definitions.html b/Function.Metric.Nat.Definitions.html
index 9cefcfe..6304c53 100644
--- a/Function.Metric.Nat.Definitions.html
+++ b/Function.Metric.Nat.Definitions.html
@@ -1,5 +1,5 @@
 
-Function.Metric.Nat.DefinitionsSource code on Github
------------------------------------------------------------------------
+Function.Metric.Nat.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core definitions for metrics over â„•
diff --git a/Function.Metric.Nat.Structures.html b/Function.Metric.Nat.Structures.html
index b51d540..018eeee 100644
--- a/Function.Metric.Nat.Structures.html
+++ b/Function.Metric.Nat.Structures.html
@@ -1,5 +1,5 @@
 
-Function.Metric.Nat.StructuresSource code on Github
------------------------------------------------------------------------
+Function.Metric.Nat.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core definitions for metrics over â„•
diff --git a/Function.Metric.Nat.html b/Function.Metric.Nat.html
index 7a99dc7..c864416 100644
--- a/Function.Metric.Nat.html
+++ b/Function.Metric.Nat.html
@@ -1,5 +1,5 @@
 
-Function.Metric.NatSource code on Github
------------------------------------------------------------------------
+Function.Metric.NatSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Metrics with â„• as the codomain of the metric function
diff --git a/Function.Metric.Structures.html b/Function.Metric.Structures.html
index 8965714..00221ae 100644
--- a/Function.Metric.Structures.html
+++ b/Function.Metric.Structures.html
@@ -1,5 +1,5 @@
 
-Function.Metric.StructuresSource code on Github
------------------------------------------------------------------------
+Function.Metric.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some metric structures (not packed up with sets, operations, etc.)
diff --git a/Function.Nary.NonDependent.Base.html b/Function.Nary.NonDependent.Base.html
index 11bd529..a60c52c 100644
--- a/Function.Nary.NonDependent.Base.html
+++ b/Function.Nary.NonDependent.Base.html
@@ -1,5 +1,5 @@
 
-Function.Nary.NonDependent.BaseSource code on Github
------------------------------------------------------------------------
+Function.Nary.NonDependent.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Heterogeneous N-ary Functions: basic types and operations
diff --git a/Function.Nary.NonDependent.html b/Function.Nary.NonDependent.html
index 0abe1ef..8980147 100644
--- a/Function.Nary.NonDependent.html
+++ b/Function.Nary.NonDependent.html
@@ -1,5 +1,5 @@
 
-Function.Nary.NonDependentSource code on Github
------------------------------------------------------------------------
+Function.Nary.NonDependentSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Heterogeneous N-ary Functions
diff --git a/Function.Properties.Bijection.html b/Function.Properties.Bijection.html
index f4aaaa0..85a1af2 100644
--- a/Function.Properties.Bijection.html
+++ b/Function.Properties.Bijection.html
@@ -1,5 +1,5 @@
 
-Function.Properties.BijectionSource code on Github
------------------------------------------------------------------------
+Function.Properties.BijectionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some basic properties of bijections.
diff --git a/Function.Properties.Inverse.HalfAdjointEquivalence.html b/Function.Properties.Inverse.HalfAdjointEquivalence.html
index 146c909..0add927 100644
--- a/Function.Properties.Inverse.HalfAdjointEquivalence.html
+++ b/Function.Properties.Inverse.HalfAdjointEquivalence.html
@@ -1,5 +1,5 @@
 
-Function.Properties.Inverse.HalfAdjointEquivalenceSource code on Github
------------------------------------------------------------------------
+Function.Properties.Inverse.HalfAdjointEquivalenceSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Half adjoint equivalences
diff --git a/Function.Properties.Inverse.html b/Function.Properties.Inverse.html
index 3b783dd..2da1e9a 100644
--- a/Function.Properties.Inverse.html
+++ b/Function.Properties.Inverse.html
@@ -1,5 +1,5 @@
 
-Function.Properties.InverseSource code on Github
------------------------------------------------------------------------
+Function.Properties.InverseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of inverses.
diff --git a/Function.Properties.RightInverse.html b/Function.Properties.RightInverse.html
index b307567..d645004 100644
--- a/Function.Properties.RightInverse.html
+++ b/Function.Properties.RightInverse.html
@@ -1,5 +1,5 @@
 
-Function.Properties.RightInverseSource code on Github
------------------------------------------------------------------------
+Function.Properties.RightInverseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of right inverses
diff --git a/Function.Properties.Surjection.html b/Function.Properties.Surjection.html
index c82dbc4..336716d 100644
--- a/Function.Properties.Surjection.html
+++ b/Function.Properties.Surjection.html
@@ -1,5 +1,5 @@
 
-Function.Properties.SurjectionSource code on Github
------------------------------------------------------------------------
+Function.Properties.SurjectionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of surjections
diff --git a/Function.Related.Propositional.html b/Function.Related.Propositional.html
index aa89d48..dd4c650 100644
--- a/Function.Related.Propositional.html
+++ b/Function.Related.Propositional.html
@@ -1,5 +1,5 @@
 
-Function.Related.PropositionalSource code on Github
------------------------------------------------------------------------
+Function.Related.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Relatedness for the function hierarchy
diff --git a/Function.Related.TypeIsomorphisms.html b/Function.Related.TypeIsomorphisms.html
index e0b27e7..7d4927b 100644
--- a/Function.Related.TypeIsomorphisms.html
+++ b/Function.Related.TypeIsomorphisms.html
@@ -1,5 +1,5 @@
 
-Function.Related.TypeIsomorphismsSource code on Github
------------------------------------------------------------------------
+Function.Related.TypeIsomorphismsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic lemmas showing that various types are related (isomorphic or
diff --git a/Function.Strict.html b/Function.Strict.html
index e686292..527b295 100644
--- a/Function.Strict.html
+++ b/Function.Strict.html
@@ -1,5 +1,5 @@
 
-Function.StrictSource code on Github
------------------------------------------------------------------------
+Function.StrictSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Strict combinators (i.e. that use call-by-value)
diff --git a/Function.Structures.Biased.html b/Function.Structures.Biased.html
index f3edd72..507536c 100644
--- a/Function.Structures.Biased.html
+++ b/Function.Structures.Biased.html
@@ -1,5 +1,5 @@
 
-Function.Structures.BiasedSource code on Github
------------------------------------------------------------------------
+Function.Structures.BiasedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Ways to give instances of certain structures where some fields can
diff --git a/Function.Structures.html b/Function.Structures.html
index 9ebd0f2..0a2e84e 100644
--- a/Function.Structures.html
+++ b/Function.Structures.html
@@ -1,5 +1,5 @@
 
-Function.StructuresSource code on Github
------------------------------------------------------------------------
+Function.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Structures for types of functions
diff --git a/Function.html b/Function.html
index 367814b..3e0f9b4 100644
--- a/Function.html
+++ b/Function.html
@@ -1,5 +1,5 @@
 
-FunctionSource code on Github
------------------------------------------------------------------------
+FunctionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Functions
diff --git a/Induction.Lexicographic.html b/Induction.Lexicographic.html
index 5fab17e..57c9237 100644
--- a/Induction.Lexicographic.html
+++ b/Induction.Lexicographic.html
@@ -1,5 +1,5 @@
 
-Induction.LexicographicSource code on Github
------------------------------------------------------------------------
+Induction.LexicographicSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lexicographic induction
diff --git a/Induction.WellFounded.html b/Induction.WellFounded.html
index 3a4870f..98f5204 100644
--- a/Induction.WellFounded.html
+++ b/Induction.WellFounded.html
@@ -1,5 +1,5 @@
 
-Induction.WellFoundedSource code on Github
------------------------------------------------------------------------
+Induction.WellFoundedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Well-founded induction
diff --git a/Induction.html b/Induction.html
index af77bb7..67bdbc7 100644
--- a/Induction.html
+++ b/Induction.html
@@ -1,5 +1,5 @@
 
-InductionSource code on Github
------------------------------------------------------------------------
+InductionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An abstraction of various forms of recursion/induction
diff --git a/Level.html b/Level.html
index 96244b0..4bc818c 100644
--- a/Level.html
+++ b/Level.html
@@ -1,5 +1,5 @@
 
-LevelSource code on Github
------------------------------------------------------------------------
+LevelSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Universe levels
diff --git a/Reflection.AST.Abstraction.html b/Reflection.AST.Abstraction.html
index 62a76ef..cf6b0f6 100644
--- a/Reflection.AST.Abstraction.html
+++ b/Reflection.AST.Abstraction.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.AbstractionSource code on Github
------------------------------------------------------------------------
+Reflection.AST.AbstractionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Abstractions used in the reflection machinery
diff --git a/Reflection.AST.Argument.Information.html b/Reflection.AST.Argument.Information.html
index dad9818..0ab0441 100644
--- a/Reflection.AST.Argument.Information.html
+++ b/Reflection.AST.Argument.Information.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.Argument.InformationSource code on Github
------------------------------------------------------------------------
+Reflection.AST.Argument.InformationSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Argument information used in the reflection machinery
diff --git a/Reflection.AST.Argument.Modality.html b/Reflection.AST.Argument.Modality.html
index e9ed92e..9c7cbeb 100644
--- a/Reflection.AST.Argument.Modality.html
+++ b/Reflection.AST.Argument.Modality.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.Argument.ModalitySource code on Github
------------------------------------------------------------------------
+Reflection.AST.Argument.ModalitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Modalities used in the reflection machinery
diff --git a/Reflection.AST.Argument.Quantity.html b/Reflection.AST.Argument.Quantity.html
index 4605f1d..7427e1f 100644
--- a/Reflection.AST.Argument.Quantity.html
+++ b/Reflection.AST.Argument.Quantity.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.Argument.QuantitySource code on Github
------------------------------------------------------------------------
+Reflection.AST.Argument.QuantitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Argument quantities used in the reflection machinery
diff --git a/Reflection.AST.Argument.Relevance.html b/Reflection.AST.Argument.Relevance.html
index 33e80c8..216c8e1 100644
--- a/Reflection.AST.Argument.Relevance.html
+++ b/Reflection.AST.Argument.Relevance.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.Argument.RelevanceSource code on Github
------------------------------------------------------------------------
+Reflection.AST.Argument.RelevanceSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Argument relevance used in the reflection machinery
diff --git a/Reflection.AST.Argument.Visibility.html b/Reflection.AST.Argument.Visibility.html
index ca6a9b7..f5d6ff2 100644
--- a/Reflection.AST.Argument.Visibility.html
+++ b/Reflection.AST.Argument.Visibility.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.Argument.VisibilitySource code on Github
------------------------------------------------------------------------
+Reflection.AST.Argument.VisibilitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Argument visibility used in the reflection machinery
diff --git a/Reflection.AST.Argument.html b/Reflection.AST.Argument.html
index c5babb4..93f1df1 100644
--- a/Reflection.AST.Argument.html
+++ b/Reflection.AST.Argument.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.ArgumentSource code on Github
------------------------------------------------------------------------
+Reflection.AST.ArgumentSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Arguments used in the reflection machinery
diff --git a/Reflection.AST.Definition.html b/Reflection.AST.Definition.html
index d8dfe71..db8db1f 100644
--- a/Reflection.AST.Definition.html
+++ b/Reflection.AST.Definition.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.DefinitionSource code on Github
------------------------------------------------------------------------
+Reflection.AST.DefinitionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions used in the reflection machinery
diff --git a/Reflection.AST.Literal.html b/Reflection.AST.Literal.html
index 87c0bf6..49d1f79 100644
--- a/Reflection.AST.Literal.html
+++ b/Reflection.AST.Literal.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.LiteralSource code on Github
------------------------------------------------------------------------
+Reflection.AST.LiteralSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Literals used in the reflection machinery
diff --git a/Reflection.AST.Meta.html b/Reflection.AST.Meta.html
index 31959c3..751963d 100644
--- a/Reflection.AST.Meta.html
+++ b/Reflection.AST.Meta.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.MetaSource code on Github
------------------------------------------------------------------------
+Reflection.AST.MetaSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Metavariables used in the reflection machinery
diff --git a/Reflection.AST.Name.html b/Reflection.AST.Name.html
index e1f3518..0ee8498 100644
--- a/Reflection.AST.Name.html
+++ b/Reflection.AST.Name.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.NameSource code on Github
------------------------------------------------------------------------
+Reflection.AST.NameSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Names used in the reflection machinery
diff --git a/Reflection.AST.Pattern.html b/Reflection.AST.Pattern.html
index 88aeb9d..e051185 100644
--- a/Reflection.AST.Pattern.html
+++ b/Reflection.AST.Pattern.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.PatternSource code on Github
------------------------------------------------------------------------
+Reflection.AST.PatternSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Patterns used in the reflection machinery
diff --git a/Reflection.AST.Show.html b/Reflection.AST.Show.html
index ff36c55..e615bae 100644
--- a/Reflection.AST.Show.html
+++ b/Reflection.AST.Show.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.ShowSource code on Github
------------------------------------------------------------------------
+Reflection.AST.ShowSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Converting reflection machinery to strings
diff --git a/Reflection.AST.Term.html b/Reflection.AST.Term.html
index 6e905c3..954ed7a 100644
--- a/Reflection.AST.Term.html
+++ b/Reflection.AST.Term.html
@@ -1,5 +1,5 @@
 
-Reflection.AST.TermSource code on Github
------------------------------------------------------------------------
+Reflection.AST.TermSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Terms used in the reflection machinery
diff --git a/Reflection.AST.html b/Reflection.AST.html
index 448578b..6e43b1a 100644
--- a/Reflection.AST.html
+++ b/Reflection.AST.html
@@ -1,5 +1,5 @@
 
-Reflection.ASTSource code on Github
------------------------------------------------------------------------
+Reflection.ASTSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The reflected abstract syntax tree
diff --git a/Reflection.TCM.Format.html b/Reflection.TCM.Format.html
index 1aacaea..a6cf7bd 100644
--- a/Reflection.TCM.Format.html
+++ b/Reflection.TCM.Format.html
@@ -1,5 +1,5 @@
 
-Reflection.TCM.FormatSource code on Github
------------------------------------------------------------------------
+Reflection.TCM.FormatSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Printf-style versions of typeError and debugPrint
diff --git a/Reflection.TCM.Syntax.html b/Reflection.TCM.Syntax.html
index 726b0ac..9d522b9 100644
--- a/Reflection.TCM.Syntax.html
+++ b/Reflection.TCM.Syntax.html
@@ -1,5 +1,5 @@
 
-Reflection.TCM.SyntaxSource code on Github
------------------------------------------------------------------------
+Reflection.TCM.SyntaxSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Monad syntax for the TC monad
diff --git a/Reflection.TCM.html b/Reflection.TCM.html
index 03730eb..130b05b 100644
--- a/Reflection.TCM.html
+++ b/Reflection.TCM.html
@@ -1,5 +1,5 @@
 
-Reflection.TCMSource code on Github
------------------------------------------------------------------------
+Reflection.TCMSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The TC (Type Checking) monad
diff --git a/Reflection.html b/Reflection.html
index 0649b24..588c5eb 100644
--- a/Reflection.html
+++ b/Reflection.html
@@ -1,5 +1,5 @@
 
-ReflectionSource code on Github
------------------------------------------------------------------------
+ReflectionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Support for reflection
diff --git a/Relation.Binary.Bundles.html b/Relation.Binary.Bundles.html
index 7b4b9a5..9339c1e 100644
--- a/Relation.Binary.Bundles.html
+++ b/Relation.Binary.Bundles.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.BundlesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for homogeneous binary relations
diff --git a/Relation.Binary.Consequences.html b/Relation.Binary.Consequences.html
index d87aa50..33965a5 100644
--- a/Relation.Binary.Consequences.html
+++ b/Relation.Binary.Consequences.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.ConsequencesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.ConsequencesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some properties imply others
diff --git a/Relation.Binary.Construct.Closure.Reflexive.Properties.html b/Relation.Binary.Construct.Closure.Reflexive.Properties.html
index b8d75e0..f416ac9 100644
--- a/Relation.Binary.Construct.Closure.Reflexive.Properties.html
+++ b/Relation.Binary.Construct.Closure.Reflexive.Properties.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.Closure.Reflexive.PropertiesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.Closure.Reflexive.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Some properties of reflexive closures
diff --git a/Relation.Binary.Construct.Closure.Reflexive.html b/Relation.Binary.Construct.Closure.Reflexive.html
index c8f0543..94cb180 100644
--- a/Relation.Binary.Construct.Closure.Reflexive.html
+++ b/Relation.Binary.Construct.Closure.Reflexive.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.Closure.ReflexiveSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.Closure.ReflexiveSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Reflexive closures
diff --git a/Relation.Binary.Construct.Composition.html b/Relation.Binary.Construct.Composition.html
index ff39468..1bb8a8e 100644
--- a/Relation.Binary.Construct.Composition.html
+++ b/Relation.Binary.Construct.Composition.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.CompositionSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.CompositionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Composition of two binary relations
diff --git a/Relation.Binary.Construct.Constant.Core.html b/Relation.Binary.Construct.Constant.Core.html
index c97a66d..84bb423 100644
--- a/Relation.Binary.Construct.Constant.Core.html
+++ b/Relation.Binary.Construct.Constant.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.Constant.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.Constant.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The binary relation defined by a constant
diff --git a/Relation.Binary.Construct.Flip.EqAndOrd.html b/Relation.Binary.Construct.Flip.EqAndOrd.html
index 7abc361..22b2652 100644
--- a/Relation.Binary.Construct.Flip.EqAndOrd.html
+++ b/Relation.Binary.Construct.Flip.EqAndOrd.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.Flip.EqAndOrdSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.Flip.EqAndOrdSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
diff --git a/Relation.Binary.Construct.Intersection.html b/Relation.Binary.Construct.Intersection.html
index 34331a6..f4722a3 100644
--- a/Relation.Binary.Construct.Intersection.html
+++ b/Relation.Binary.Construct.Intersection.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.IntersectionSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.IntersectionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Intersection of two binary relations
diff --git a/Relation.Binary.Construct.NaturalOrder.Left.html b/Relation.Binary.Construct.NaturalOrder.Left.html
index 12e9ca9..6577bd1 100644
--- a/Relation.Binary.Construct.NaturalOrder.Left.html
+++ b/Relation.Binary.Construct.NaturalOrder.Left.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.NaturalOrder.LeftSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.NaturalOrder.LeftSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Conversion of binary operators to binary relations via the left
diff --git a/Relation.Binary.Construct.NonStrictToStrict.html b/Relation.Binary.Construct.NonStrictToStrict.html
index 5ee18ab..081b4bc 100644
--- a/Relation.Binary.Construct.NonStrictToStrict.html
+++ b/Relation.Binary.Construct.NonStrictToStrict.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.NonStrictToStrictSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.NonStrictToStrictSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Conversion of _≤_ to _<_
diff --git a/Relation.Binary.Construct.On.html b/Relation.Binary.Construct.On.html
index ed7ed45..a9d6224 100644
--- a/Relation.Binary.Construct.On.html
+++ b/Relation.Binary.Construct.On.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.OnSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.OnSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Many properties which hold for `_∼_` also hold for `_∼_ on f`
diff --git a/Relation.Binary.Construct.StrictToNonStrict.html b/Relation.Binary.Construct.StrictToNonStrict.html
index 0ae98d0..23b9609 100644
--- a/Relation.Binary.Construct.StrictToNonStrict.html
+++ b/Relation.Binary.Construct.StrictToNonStrict.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.StrictToNonStrictSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.StrictToNonStrictSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Conversion of < to ≤, along with a number of properties
diff --git a/Relation.Binary.Construct.Subst.Equality.html b/Relation.Binary.Construct.Subst.Equality.html
index 5154879..2ea8856 100644
--- a/Relation.Binary.Construct.Subst.Equality.html
+++ b/Relation.Binary.Construct.Subst.Equality.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Construct.Subst.EqualitySource code on Github
------------------------------------------------------------------------
+Relation.Binary.Construct.Subst.EqualitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Substituting equalities for binary relations
diff --git a/Relation.Binary.Core.html b/Relation.Binary.Core.html
index 3e4970b..6d67bf1 100644
--- a/Relation.Binary.Core.html
+++ b/Relation.Binary.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Binary.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of binary relations
diff --git a/Relation.Binary.Definitions.html b/Relation.Binary.Definitions.html
index 2296523..1298fff 100644
--- a/Relation.Binary.Definitions.html
+++ b/Relation.Binary.Definitions.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.DefinitionsSource code on Github
------------------------------------------------------------------------
+Relation.Binary.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of binary relations
diff --git a/Relation.Binary.Indexed.Heterogeneous.Bundles.html b/Relation.Binary.Indexed.Heterogeneous.Bundles.html
index 17ba490..fd52d4d 100644
--- a/Relation.Binary.Indexed.Heterogeneous.Bundles.html
+++ b/Relation.Binary.Indexed.Heterogeneous.Bundles.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.Heterogeneous.BundlesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.Heterogeneous.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Indexed binary relations
diff --git a/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html b/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html
index 769fb9a..52dc7ab 100644
--- a/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html
+++ b/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.Heterogeneous.Construct.TrivialSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.Heterogeneous.Construct.TrivialSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Creates trivially indexed records from their non-indexed counterpart.
diff --git a/Relation.Binary.Indexed.Heterogeneous.Core.html b/Relation.Binary.Indexed.Heterogeneous.Core.html
index 2aacaf3..41d49d6 100644
--- a/Relation.Binary.Indexed.Heterogeneous.Core.html
+++ b/Relation.Binary.Indexed.Heterogeneous.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.Heterogeneous.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.Heterogeneous.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Indexed binary relations
diff --git a/Relation.Binary.Indexed.Heterogeneous.Definitions.html b/Relation.Binary.Indexed.Heterogeneous.Definitions.html
index 0789673..0ed2975 100644
--- a/Relation.Binary.Indexed.Heterogeneous.Definitions.html
+++ b/Relation.Binary.Indexed.Heterogeneous.Definitions.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.Heterogeneous.DefinitionsSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.Heterogeneous.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Indexed binary relations
diff --git a/Relation.Binary.Indexed.Heterogeneous.Structures.html b/Relation.Binary.Indexed.Heterogeneous.Structures.html
index 52fe7e4..3425963 100644
--- a/Relation.Binary.Indexed.Heterogeneous.Structures.html
+++ b/Relation.Binary.Indexed.Heterogeneous.Structures.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.Heterogeneous.StructuresSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.Heterogeneous.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Indexed binary relations
diff --git a/Relation.Binary.Indexed.Heterogeneous.html b/Relation.Binary.Indexed.Heterogeneous.html
index 6fbfeb0..f8daad1 100644
--- a/Relation.Binary.Indexed.Heterogeneous.html
+++ b/Relation.Binary.Indexed.Heterogeneous.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Indexed.HeterogeneousSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Indexed.HeterogeneousSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Heterogeneously-indexed binary relations
diff --git a/Relation.Binary.Lattice.Bundles.html b/Relation.Binary.Lattice.Bundles.html
index 36dcdd9..9293383 100644
--- a/Relation.Binary.Lattice.Bundles.html
+++ b/Relation.Binary.Lattice.Bundles.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Lattice.BundlesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Lattice.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for order-theoretic lattices
diff --git a/Relation.Binary.Lattice.Definitions.html b/Relation.Binary.Lattice.Definitions.html
index 2c3340d..eb654af 100644
--- a/Relation.Binary.Lattice.Definitions.html
+++ b/Relation.Binary.Lattice.Definitions.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Lattice.DefinitionsSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Lattice.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Definitions for order-theoretic lattices
diff --git a/Relation.Binary.Lattice.Structures.html b/Relation.Binary.Lattice.Structures.html
index b4ec12f..fd78cfa 100644
--- a/Relation.Binary.Lattice.Structures.html
+++ b/Relation.Binary.Lattice.Structures.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Lattice.StructuresSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Lattice.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Structures for order-theoretic lattices
diff --git a/Relation.Binary.Lattice.html b/Relation.Binary.Lattice.html
index 018d16a..e085461 100644
--- a/Relation.Binary.Lattice.html
+++ b/Relation.Binary.Lattice.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.LatticeSource code on Github
------------------------------------------------------------------------
+Relation.Binary.LatticeSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Order-theoretic lattices
diff --git a/Relation.Binary.Morphism.Bundles.html b/Relation.Binary.Morphism.Bundles.html
index 882f261..1969f0a 100644
--- a/Relation.Binary.Morphism.Bundles.html
+++ b/Relation.Binary.Morphism.Bundles.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Morphism.BundlesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Morphism.BundlesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Bundles for morphisms between binary relations
diff --git a/Relation.Binary.Morphism.Definitions.html b/Relation.Binary.Morphism.Definitions.html
index da7c26a..5226d0c 100644
--- a/Relation.Binary.Morphism.Definitions.html
+++ b/Relation.Binary.Morphism.Definitions.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Morphism.DefinitionsSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Morphism.DefinitionsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Basic definitions for morphisms between algebraic structures
diff --git a/Relation.Binary.Morphism.OrderMonomorphism.html b/Relation.Binary.Morphism.OrderMonomorphism.html
index 1468b07..27eee04 100644
--- a/Relation.Binary.Morphism.OrderMonomorphism.html
+++ b/Relation.Binary.Morphism.OrderMonomorphism.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Morphism.OrderMonomorphismSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Morphism.OrderMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between orders
diff --git a/Relation.Binary.Morphism.RelMonomorphism.html b/Relation.Binary.Morphism.RelMonomorphism.html
index c44f349..14668fe 100644
--- a/Relation.Binary.Morphism.RelMonomorphism.html
+++ b/Relation.Binary.Morphism.RelMonomorphism.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Morphism.RelMonomorphismSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Morphism.RelMonomorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Consequences of a monomorphism between binary relations
diff --git a/Relation.Binary.Morphism.Structures.html b/Relation.Binary.Morphism.Structures.html
index 03c5446..f11c596 100644
--- a/Relation.Binary.Morphism.Structures.html
+++ b/Relation.Binary.Morphism.Structures.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Morphism.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Order morphisms
diff --git a/Relation.Binary.Morphism.html b/Relation.Binary.Morphism.html
index 4359cdf..b07e12d 100644
--- a/Relation.Binary.Morphism.html
+++ b/Relation.Binary.Morphism.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.MorphismSource code on Github
------------------------------------------------------------------------
+Relation.Binary.MorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Order morphisms
diff --git a/Relation.Binary.Properties.ApartnessRelation.html b/Relation.Binary.Properties.ApartnessRelation.html
index 480e637..e4e7e5f 100644
--- a/Relation.Binary.Properties.ApartnessRelation.html
+++ b/Relation.Binary.Properties.ApartnessRelation.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.ApartnessRelationSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.ApartnessRelationSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Apartness properties
diff --git a/Relation.Binary.Properties.DecSetoid.html b/Relation.Binary.Properties.DecSetoid.html
index 1b711f2..c06c01e 100644
--- a/Relation.Binary.Properties.DecSetoid.html
+++ b/Relation.Binary.Properties.DecSetoid.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.DecSetoidSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.DecSetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Every decidable setoid induces tight apartness relation.
diff --git a/Relation.Binary.Properties.DecTotalOrder.html b/Relation.Binary.Properties.DecTotalOrder.html
index 13fd5b4..e02b031 100644
--- a/Relation.Binary.Properties.DecTotalOrder.html
+++ b/Relation.Binary.Properties.DecTotalOrder.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.DecTotalOrderSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.DecTotalOrderSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties satisfied by decidable total orders
diff --git a/Relation.Binary.Properties.Poset.html b/Relation.Binary.Properties.Poset.html
index 492bc87..43c9d71 100644
--- a/Relation.Binary.Properties.Poset.html
+++ b/Relation.Binary.Properties.Poset.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.PosetSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.PosetSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties satisfied by posets
diff --git a/Relation.Binary.Properties.Preorder.html b/Relation.Binary.Properties.Preorder.html
index 2641ae3..3a70a29 100644
--- a/Relation.Binary.Properties.Preorder.html
+++ b/Relation.Binary.Properties.Preorder.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.PreorderSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.PreorderSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties satisfied by preorders
diff --git a/Relation.Binary.Properties.Setoid.html b/Relation.Binary.Properties.Setoid.html
index 943a74a..a1e0595 100644
--- a/Relation.Binary.Properties.Setoid.html
+++ b/Relation.Binary.Properties.Setoid.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.SetoidSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Additional properties for setoids
diff --git a/Relation.Binary.Properties.TotalOrder.html b/Relation.Binary.Properties.TotalOrder.html
index 457ddc6..8eb4aae 100644
--- a/Relation.Binary.Properties.TotalOrder.html
+++ b/Relation.Binary.Properties.TotalOrder.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Properties.TotalOrderSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Properties.TotalOrderSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties satisfied by total orders
diff --git a/Relation.Binary.PropositionalEquality.Algebra.html b/Relation.Binary.PropositionalEquality.Algebra.html
index 1673e13..ba5546b 100644
--- a/Relation.Binary.PropositionalEquality.Algebra.html
+++ b/Relation.Binary.PropositionalEquality.Algebra.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.PropositionalEquality.AlgebraSource code on Github
------------------------------------------------------------------------
+Relation.Binary.PropositionalEquality.AlgebraSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Propositional (intensional) equality - Algebraic structures
diff --git a/Relation.Binary.PropositionalEquality.Core.html b/Relation.Binary.PropositionalEquality.Core.html
index 7aece62..e72ac2e 100644
--- a/Relation.Binary.PropositionalEquality.Core.html
+++ b/Relation.Binary.PropositionalEquality.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.PropositionalEquality.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Binary.PropositionalEquality.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Propositional equality
diff --git a/Relation.Binary.PropositionalEquality.Properties.html b/Relation.Binary.PropositionalEquality.Properties.html
index 8726347..c8c5223 100644
--- a/Relation.Binary.PropositionalEquality.Properties.html
+++ b/Relation.Binary.PropositionalEquality.Properties.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.PropositionalEquality.PropertiesSource code on Github
------------------------------------------------------------------------
+Relation.Binary.PropositionalEquality.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Propositional equality
diff --git a/Relation.Binary.PropositionalEquality.html b/Relation.Binary.PropositionalEquality.html
index c4d48a7..30bf22b 100644
--- a/Relation.Binary.PropositionalEquality.html
+++ b/Relation.Binary.PropositionalEquality.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.PropositionalEqualitySource code on Github
------------------------------------------------------------------------
+Relation.Binary.PropositionalEqualitySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Propositional (intensional) equality
diff --git a/Relation.Binary.Reasoning.Base.Double.html b/Relation.Binary.Reasoning.Base.Double.html
index 22ad537..caae8a0 100644
--- a/Relation.Binary.Reasoning.Base.Double.html
+++ b/Relation.Binary.Reasoning.Base.Double.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.Base.DoubleSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.Base.DoubleSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The basic code for equational reasoning with two relations:
diff --git a/Relation.Binary.Reasoning.Base.Single.html b/Relation.Binary.Reasoning.Base.Single.html
index 6b894a6..8c80217 100644
--- a/Relation.Binary.Reasoning.Base.Single.html
+++ b/Relation.Binary.Reasoning.Base.Single.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.Base.SingleSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.Base.SingleSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The basic code for equational reasoning with a single relation
diff --git a/Relation.Binary.Reasoning.Base.Triple.html b/Relation.Binary.Reasoning.Base.Triple.html
index 6f96492..0fcc95a 100644
--- a/Relation.Binary.Reasoning.Base.Triple.html
+++ b/Relation.Binary.Reasoning.Base.Triple.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.Base.TripleSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.Base.TripleSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The basic code for equational reasoning with three relations:
diff --git a/Relation.Binary.Reasoning.Preorder.html b/Relation.Binary.Reasoning.Preorder.html
index ea62b5d..7d47b7a 100644
--- a/Relation.Binary.Reasoning.Preorder.html
+++ b/Relation.Binary.Reasoning.Preorder.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.PreorderSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.PreorderSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Convenient syntax for "equational reasoning" using a preorder
diff --git a/Relation.Binary.Reasoning.Setoid.html b/Relation.Binary.Reasoning.Setoid.html
index 3d326bd..c7b5684 100644
--- a/Relation.Binary.Reasoning.Setoid.html
+++ b/Relation.Binary.Reasoning.Setoid.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.SetoidSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Convenient syntax for reasoning with a setoid
diff --git a/Relation.Binary.Reasoning.Syntax.html b/Relation.Binary.Reasoning.Syntax.html
index 88fa8d4..6fe1779 100644
--- a/Relation.Binary.Reasoning.Syntax.html
+++ b/Relation.Binary.Reasoning.Syntax.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Reasoning.SyntaxSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Reasoning.SyntaxSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Syntax for the building blocks of equational reasoning modules
diff --git a/Relation.Binary.Reflection.html b/Relation.Binary.Reflection.html
index fbb84bb..e3d71d5 100644
--- a/Relation.Binary.Reflection.html
+++ b/Relation.Binary.Reflection.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.ReflectionSource code on Github
------------------------------------------------------------------------
+Relation.Binary.ReflectionSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Helpers intended to ease the development of "tactics" which use
diff --git a/Relation.Binary.Structures.Biased.html b/Relation.Binary.Structures.Biased.html
index 06e9117..6ef65a9 100644
--- a/Relation.Binary.Structures.Biased.html
+++ b/Relation.Binary.Structures.Biased.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.Structures.BiasedSource code on Github
------------------------------------------------------------------------
+Relation.Binary.Structures.BiasedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Ways to give instances of certain structures where some fields can
diff --git a/Relation.Binary.Structures.html b/Relation.Binary.Structures.html
index 898b921..c3a2ec6 100644
--- a/Relation.Binary.Structures.html
+++ b/Relation.Binary.Structures.html
@@ -1,5 +1,5 @@
 
-Relation.Binary.StructuresSource code on Github
------------------------------------------------------------------------
+Relation.Binary.StructuresSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Structures for homogeneous binary relations
diff --git a/Relation.Binary.html b/Relation.Binary.html
index fdeb931..f26d6b4 100644
--- a/Relation.Binary.html
+++ b/Relation.Binary.html
@@ -1,5 +1,5 @@
 
-Relation.BinarySource code on Github
------------------------------------------------------------------------
+Relation.BinarySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of homogeneous binary relations
diff --git a/Relation.Nullary.Decidable.Core.html b/Relation.Nullary.Decidable.Core.html
index b8003e1..58036d8 100644
--- a/Relation.Nullary.Decidable.Core.html
+++ b/Relation.Nullary.Decidable.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.Decidable.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.Decidable.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Operations on and properties of decidable relations
diff --git a/Relation.Nullary.Decidable.html b/Relation.Nullary.Decidable.html
index 2f395e3..cbf8902 100644
--- a/Relation.Nullary.Decidable.html
+++ b/Relation.Nullary.Decidable.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.DecidableSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.DecidableSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Operations on and properties of decidable relations
diff --git a/Relation.Nullary.Indexed.html b/Relation.Nullary.Indexed.html
index 8870a98..14f8549 100644
--- a/Relation.Nullary.Indexed.html
+++ b/Relation.Nullary.Indexed.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.IndexedSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.IndexedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Negation indexed by a Level
diff --git a/Relation.Nullary.Negation.Core.html b/Relation.Nullary.Negation.Core.html
index aeba8db..5cffb91 100644
--- a/Relation.Nullary.Negation.Core.html
+++ b/Relation.Nullary.Negation.Core.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.Negation.CoreSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.Negation.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Core properties related to negation
diff --git a/Relation.Nullary.Negation.html b/Relation.Nullary.Negation.html
index 7baddfd..57626e8 100644
--- a/Relation.Nullary.Negation.html
+++ b/Relation.Nullary.Negation.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.NegationSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.NegationSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to negation
diff --git a/Relation.Nullary.Recomputable.html b/Relation.Nullary.Recomputable.html
index 7f67ac8..d1c5469 100644
--- a/Relation.Nullary.Recomputable.html
+++ b/Relation.Nullary.Recomputable.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.RecomputableSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.RecomputableSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Recomputable types and their algebra as Harrop formulas
diff --git a/Relation.Nullary.Reflects.html b/Relation.Nullary.Reflects.html
index 9f7fb1b..f1f21ee 100644
--- a/Relation.Nullary.Reflects.html
+++ b/Relation.Nullary.Reflects.html
@@ -1,5 +1,5 @@
 
-Relation.Nullary.ReflectsSource code on Github
------------------------------------------------------------------------
+Relation.Nullary.ReflectsSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of the `Reflects` construct
diff --git a/Relation.Nullary.html b/Relation.Nullary.html
index 1f7dfac..0b27608 100644
--- a/Relation.Nullary.html
+++ b/Relation.Nullary.html
@@ -1,5 +1,5 @@
 
-Relation.NullarySource code on Github
------------------------------------------------------------------------
+Relation.NullarySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Operations on nullary relations (like negation and decidability)
diff --git a/Relation.Unary.PredicateTransformer.html b/Relation.Unary.PredicateTransformer.html
index ac74cdf..1aa299a 100644
--- a/Relation.Unary.PredicateTransformer.html
+++ b/Relation.Unary.PredicateTransformer.html
@@ -1,5 +1,5 @@
 
-Relation.Unary.PredicateTransformerSource code on Github
------------------------------------------------------------------------
+Relation.Unary.PredicateTransformerSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Predicate transformers
diff --git a/Relation.Unary.Properties.html b/Relation.Unary.Properties.html
index a4f611e..1558789 100644
--- a/Relation.Unary.Properties.html
+++ b/Relation.Unary.Properties.html
@@ -1,5 +1,5 @@
 
-Relation.Unary.PropertiesSource code on Github
------------------------------------------------------------------------
+Relation.Unary.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of constructions over unary relations
diff --git a/Relation.Unary.html b/Relation.Unary.html
index fc5235a..bebf88d 100644
--- a/Relation.Unary.html
+++ b/Relation.Unary.html
@@ -1,5 +1,5 @@
 
-Relation.UnarySource code on Github
------------------------------------------------------------------------
+Relation.UnarySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Unary relations
diff --git a/Test.DecEq.html b/Test.DecEq.html
index aeff28f..89ed9d3 100644
--- a/Test.DecEq.html
+++ b/Test.DecEq.html
@@ -1,5 +1,5 @@
 
-Test.DecEqSource code on Github
{-# OPTIONS --without-K #-}
+Test.DecEqSource code on Github
{-# OPTIONS --without-K #-}
 module Test.DecEq where
 
 open import Class.Prelude
diff --git a/Test.Decidable.html b/Test.Decidable.html
index 03c2104..8ce7f4f 100644
--- a/Test.Decidable.html
+++ b/Test.Decidable.html
@@ -1,5 +1,5 @@
 
-Test.DecidableSource code on Github
{-# OPTIONS --without-K #-}
+Test.DecidableSource code on Github
{-# OPTIONS --without-K #-}
 module Test.Decidable where
 
 open import Class.Prelude
diff --git a/Test.Functor.html b/Test.Functor.html
index 2bbed8e..7a641d6 100644
--- a/Test.Functor.html
+++ b/Test.Functor.html
@@ -1,5 +1,5 @@
 
-Test.FunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Test.FunctorSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Test.Functor where
 
 open import Class.Prelude
diff --git a/Test.Monoid.html b/Test.Monoid.html
index 69a7107..10bdf98 100644
--- a/Test.Monoid.html
+++ b/Test.Monoid.html
@@ -1,5 +1,5 @@
 
-Test.MonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Test.MonoidSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Test.Monoid where
 
 open import Class.Prelude
diff --git a/Test.Show.html b/Test.Show.html
index b4f7c53..64fafd1 100644
--- a/Test.Show.html
+++ b/Test.Show.html
@@ -1,5 +1,5 @@
 
-Test.ShowSource code on Github
{-# OPTIONS --cubical-compatible #-}
+Test.ShowSource code on Github
{-# OPTIONS --cubical-compatible #-}
 module Test.Show where
 
 open import Class.Prelude
diff --git a/Text.Format.Generic.html b/Text.Format.Generic.html
index 5eba7ea..ad84f79 100644
--- a/Text.Format.Generic.html
+++ b/Text.Format.Generic.html
@@ -1,5 +1,5 @@
 
-Text.Format.GenericSource code on Github
------------------------------------------------------------------------
+Text.Format.GenericSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Format strings for Printf and Scanf
diff --git a/Text.Format.html b/Text.Format.html
index 15f32ba..1993246 100644
--- a/Text.Format.html
+++ b/Text.Format.html
@@ -1,5 +1,5 @@
 
-Text.FormatSource code on Github
------------------------------------------------------------------------
+Text.FormatSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Format strings for Printf and Scanf
diff --git a/Text.Printf.Generic.html b/Text.Printf.Generic.html
index 066470c..c0b1745 100644
--- a/Text.Printf.Generic.html
+++ b/Text.Printf.Generic.html
@@ -1,5 +1,5 @@
 
-Text.Printf.GenericSource code on Github
------------------------------------------------------------------------
+Text.Printf.GenericSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Generic printf function.
diff --git a/Text.Printf.html b/Text.Printf.html
index ec429d9..49e6168 100644
--- a/Text.Printf.html
+++ b/Text.Printf.html
@@ -1,5 +1,5 @@
 
-Text.PrintfSource code on Github
------------------------------------------------------------------------
+Text.PrintfSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Printf
diff --git a/index.html b/index.html
index 515a884..167c29e 100644
--- a/index.html
+++ b/index.html
@@ -1,5 +1,5 @@
 
-standard-library-classesSource code on Github
{-# OPTIONS --with-K #-}
+standard-library-classesSource code on Github
{-# OPTIONS --with-K #-}
 module standard-library-classes where
 
 -- ** Algebraic structures
diff --git a/standard-library-classes.html b/standard-library-classes.html
index e1a96a6..3a86d81 100644
--- a/standard-library-classes.html
+++ b/standard-library-classes.html
@@ -1,5 +1,5 @@
 
-standard-library-classesSource code on Github
{-# OPTIONS --with-K #-}
+standard-library-classesSource code on Github
{-# OPTIONS --with-K #-}
 module standard-library-classes where
 
 -- ** Algebraic structures
diff --git a/typecheck.time b/typecheck.time
index 4bbfbe9..403a038 100644
--- a/typecheck.time
+++ b/typecheck.time
@@ -1,10 +1,10 @@
-TOTAL: 0m17s
-Class/Prelude: 0m9s
+TOTAL: 0m16s
+Class/Prelude: 0m8s
 Class/Semigroup/Core: 0m0s
 Class/Semigroup/Instances: 0m1s
 Class/Semigroup: 0m0s
-Class/Monoid/Core: 0m1s
-Class/Monoid/Instances: 0m0s
+Class/Monoid/Core: 0m0s
+Class/Monoid/Instances: 0m1s
 Class/Monoid: 0m0s
 Class/CommutativeMonoid/Core: 0m0s
 Class/CommutativeMonoid/Instances: 0m0s
@@ -18,7 +18,7 @@ Class/Applicative/Core: 0m0s
 Class/Applicative/Instances: 0m0s
 Class/Applicative: 0m0s
 Class/Monad/Core: 0m0s
-Class/Monad/Instances: 0m1s
+Class/Monad/Instances: 0m0s
 Class/Monad: 0m0s
 Class/Foldable/Core: 0m0s
 Class/Foldable/Instances: 0m0s
@@ -27,15 +27,15 @@ Class/Traversable/Core: 0m0s
 Class/Traversable/Instances: 0m0s
 Class/Traversable: 0m0s
 Class/DecEq/Core: 0m0s
-Class/DecEq/Instances: 0m0s
+Class/DecEq/Instances: 0m1s
 Class/DecEq: 0m0s
 Class/DecEq/WithK: 0m0s
 Class/Decidable/Core: 0m0s
-Class/Decidable/Instances: 0m1s
+Class/Decidable/Instances: 0m0s
 Class/Decidable: 0m0s
 Class/Allable/Core: 0m0s
-Class/HasOrder/Core: 0m0s
-Class/HasOrder/Instance: 0m1s
+Class/HasOrder/Core: 0m1s
+Class/HasOrder/Instance: 0m0s
 Class/HasOrder: 0m0s
 Class/Allable/Instance: 0m0s
 Class/Allable: 0m0s
@@ -46,7 +46,7 @@ Class/Default: 0m0s
 Class/HasAdd/Core: 0m0s
 Class/HasAdd/Instance: 0m0s
 Class/HasAdd: 0m0s
-Class/Show/Core: 0m0s
+Class/Show/Core: 0m1s
 Class/Show/Instances: 0m0s
 Class/Show: 0m0s
 Class/ToBool: 0m0s