diff --git a/Agda.Builtin.Bool.html b/Agda.Builtin.Bool.html index 69f1dac..4c25624 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 6112d16..9c0aba2 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 b773e69..5250e18 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 36088a1..8fb7982 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 a199c38..166d4e9 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 25bfa83..4e5e7ef 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 5d70e19..97e8fc9 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 a98fa75..b77746f 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 232f3b6..defc8e5 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 378a8d2..64963c5 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 91c2710..3b5f014 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 630e926..dc4418c 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 eca4294..82a57c9 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 cf1cdb4..1bc0455 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 e5e3053..27ff423 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 d96fdae..f73934f 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 0b408ca..327dd34 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 96a0233..a8ec55f 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 56655de..2d28a3d 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 aacda3f..e49f64d 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 aee2b89..5970f4d 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 fd30e60..7f47927 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 add1472..124d84b 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 e6ad6c3..3db8f9e 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 5b38ec0..edd5e34 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 e78aa6e..dd423a4 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 4b75a04..ea90332 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 3740923..92eed39 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 53a3798..bafd38b 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 da2e88d..d0c1ff9 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 8a484cd..7927974 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 133d1f4..62a1d15 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 ab7b73a..1561fbc 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 f737aab..6e37c1c 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 a5659fb..18963d9 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 03fed36..0df4394 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 eb4e9c6..9ba0e89 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 ff308d1..e1ecb24 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 fe10f81..98c5013 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 850b256..c61532a 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.Function.html b/Algebra.Function.html
index 3b47ba6..b1c300b 100644
--- a/Algebra.Function.html
+++ b/Algebra.Function.html
@@ -1,5 +1,5 @@
 
-Algebra.FunctionSource code on Github
{-# OPTIONS --safe --without-K #-}
+Algebra.FunctionSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 open import Level
 open import Algebra.Lattice
diff --git a/Algebra.Lattice.Bundles.Raw.html b/Algebra.Lattice.Bundles.Raw.html
index 2b7baa1..5026d52 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 224325c..7993d1a 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 720b078..50aba74 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 161d9a8..28e1e82 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 52944b9..655ec7f 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 bc6540e..43940cb 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 f9094cc..b6ea5e6 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 7d8a88c..1108089 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 55f8839..19a714f 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 7c010ad..49a6190 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 b0a813d..b5663d4 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 9d820ba..a31faae 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 56dfdc0..87ebbd2 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 ae426a8..ac335f1 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 0d322ea..59cf7c2 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 74b7b46..46b7dab 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 15d4de0..13dfe4a 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 8faf5ac..37a735e 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 74668ac..a34f1fe 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 b29a124..b11446d 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 777c65d..42c8420 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 2e26817..c825d13 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 c46afa5..b2b8bfc 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 25c9d57..11b2406 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 3d51906..bfe8bed 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 181c5de..b793be8 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 9657543..dedb6e7 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 e8e4acd..03f0e92 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 91d07f9..e876626 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 b459dc3..c35f06e 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 09cef61..853d7fa 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 8aab06d..68a7cc5 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 30fd778..531f995 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 a4e19f3..9de9d81 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 5fa139d..aa5bf99 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 43c04c3..af93d60 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 bfc5015..b07cbbe 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 4101603..e07357b 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 a327749..b683f7e 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 0bc364b..3b948b4 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.Applicative.Core.html b/Class.Applicative.Core.html
index fe61bcb..2a5b229 100644
--- a/Class.Applicative.Core.html
+++ b/Class.Applicative.Core.html
@@ -1,5 +1,5 @@
 
-Class.Applicative.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Applicative.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Applicative.Core where
 
 open import Class.Prelude
diff --git a/Class.Applicative.Instances.html b/Class.Applicative.Instances.html
index e26756f..d0ac930 100644
--- a/Class.Applicative.Instances.html
+++ b/Class.Applicative.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Applicative.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Applicative.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Applicative.Instances where
 
 open import Class.Prelude
diff --git a/Class.Applicative.html b/Class.Applicative.html
index f6280a8..711844c 100644
--- a/Class.Applicative.html
+++ b/Class.Applicative.html
@@ -1,5 +1,5 @@
 
-Class.ApplicativeSource code on Github
{-# OPTIONS --without-K #-}
+Class.ApplicativeSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Applicative where
 
 open import Class.Applicative.Core public
diff --git a/Class.Core.html b/Class.Core.html
index 9a2d193..3dcd4a9 100644
--- a/Class.Core.html
+++ b/Class.Core.html
@@ -1,5 +1,5 @@
 
-Class.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Core where
 
 open import Class.Prelude
diff --git a/Class.DecEq.Core.html b/Class.DecEq.Core.html
index ee64de0..bef5d13 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 2b3e97d..22d64ea 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.html b/Class.DecEq.html
index 0a75b7c..04f4a55 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.Functor.Core.html b/Class.Functor.Core.html
index 7510332..83188b2 100644
--- a/Class.Functor.Core.html
+++ b/Class.Functor.Core.html
@@ -1,5 +1,5 @@
 
-Class.Functor.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Functor.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Functor.Core where
 
 open import Class.Prelude
diff --git a/Class.Functor.Instances.html b/Class.Functor.Instances.html
index 0854cc9..be3e946 100644
--- a/Class.Functor.Instances.html
+++ b/Class.Functor.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Functor.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Functor.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Functor.Instances where
 
 open import Class.Prelude
diff --git a/Class.Functor.html b/Class.Functor.html
index 1dc9698..fd1c108 100644
--- a/Class.Functor.html
+++ b/Class.Functor.html
@@ -1,5 +1,5 @@
 
-Class.FunctorSource code on Github
{-# OPTIONS --without-K #-}
+Class.FunctorSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Functor where
 
 open import Class.Functor.Core public
diff --git a/Class.Monad.Core.html b/Class.Monad.Core.html
index 5fea700..1203a3c 100644
--- a/Class.Monad.Core.html
+++ b/Class.Monad.Core.html
@@ -1,5 +1,5 @@
 
-Class.Monad.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Monad.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Monad.Core where
 
 open import Class.Prelude
diff --git a/Class.Monad.Instances.html b/Class.Monad.Instances.html
index 340029f..7c037d9 100644
--- a/Class.Monad.Instances.html
+++ b/Class.Monad.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Monad.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Monad.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Monad.Instances where
 
 open import Class.Prelude
diff --git a/Class.Monad.html b/Class.Monad.html
index 7273b47..8a5558e 100644
--- a/Class.Monad.html
+++ b/Class.Monad.html
@@ -1,5 +1,5 @@
 
-Class.MonadSource code on Github
{-# OPTIONS --without-K #-}
+Class.MonadSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Monad where
 
 open import Class.Monad.Core public
diff --git a/Class.MonadError.Instances.html b/Class.MonadError.Instances.html
index 2d509ac..460b814 100644
--- a/Class.MonadError.Instances.html
+++ b/Class.MonadError.Instances.html
@@ -1,5 +1,5 @@
 
-Class.MonadError.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadError.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Class.MonadError.Instances where
 
 open import Class.MonadError public
diff --git a/Class.MonadError.html b/Class.MonadError.html
index 1f3d942..23ca3bd 100644
--- a/Class.MonadError.html
+++ b/Class.MonadError.html
@@ -1,5 +1,5 @@
 
-Class.MonadErrorSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadErrorSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 open import Level
 
diff --git a/Class.MonadReader.Instances.html b/Class.MonadReader.Instances.html
index 67c40a1..a5b2363 100644
--- a/Class.MonadReader.Instances.html
+++ b/Class.MonadReader.Instances.html
@@ -1,5 +1,5 @@
 
-Class.MonadReader.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadReader.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Class.MonadReader.Instances where
 
 open import Class.MonadReader public
diff --git a/Class.MonadReader.html b/Class.MonadReader.html
index 2d74e96..27b5750 100644
--- a/Class.MonadReader.html
+++ b/Class.MonadReader.html
@@ -1,5 +1,5 @@
 
-Class.MonadReaderSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadReaderSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Class.MonadReader where
 
diff --git a/Class.MonadTC.Instances.html b/Class.MonadTC.Instances.html
index 2977309..3e6ca6c 100644
--- a/Class.MonadTC.Instances.html
+++ b/Class.MonadTC.Instances.html
@@ -1,5 +1,5 @@
 
-Class.MonadTC.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadTC.InstancesSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Class.MonadTC.Instances where
 
 open import Class.MonadTC public
diff --git a/Class.MonadTC.html b/Class.MonadTC.html
index e77204b..0ea83ef 100644
--- a/Class.MonadTC.html
+++ b/Class.MonadTC.html
@@ -1,5 +1,5 @@
 
-Class.MonadTCSource code on Github
{-# OPTIONS --safe --without-K #-}
+Class.MonadTCSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Class.MonadTC where
 
diff --git a/Class.Prelude.html b/Class.Prelude.html
index 4f97f57..9530bd6 100644
--- a/Class.Prelude.html
+++ b/Class.Prelude.html
@@ -1,5 +1,5 @@
 
-Class.PreludeSource code on Github
{-# OPTIONS --without-K #-}
+Class.PreludeSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Prelude where
 
 open import Agda.Primitive public
diff --git a/Class.Semigroup.Core.html b/Class.Semigroup.Core.html
index 62f339c..8645950 100644
--- a/Class.Semigroup.Core.html
+++ b/Class.Semigroup.Core.html
@@ -1,5 +1,5 @@
 
-Class.Semigroup.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Semigroup.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Semigroup.Core where
 
 open import Class.Prelude
diff --git a/Class.Semigroup.Instances.html b/Class.Semigroup.Instances.html
index 0fb0f61..857eeb4 100644
--- a/Class.Semigroup.Instances.html
+++ b/Class.Semigroup.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Semigroup.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Semigroup.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Semigroup.Instances where
 
 open import Class.Prelude
diff --git a/Class.Semigroup.html b/Class.Semigroup.html
index 788baf5..fea5697 100644
--- a/Class.Semigroup.html
+++ b/Class.Semigroup.html
@@ -1,5 +1,5 @@
 
-Class.SemigroupSource code on Github
{-# OPTIONS --without-K #-}
+Class.SemigroupSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Semigroup where
 
 open import Class.Semigroup.Core public
diff --git a/Class.Show.Core.html b/Class.Show.Core.html
index 46b2047..8515e4f 100644
--- a/Class.Show.Core.html
+++ b/Class.Show.Core.html
@@ -1,5 +1,5 @@
 
-Class.Show.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Show.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Show.Core where
 
 open import Class.Prelude
diff --git a/Class.Show.Instances.html b/Class.Show.Instances.html
index 6142f28..181c8cd 100644
--- a/Class.Show.Instances.html
+++ b/Class.Show.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Show.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Show.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Show.Instances where
 
 open import Class.Prelude hiding (Type)
diff --git a/Class.Show.html b/Class.Show.html
index 15c689c..2344428 100644
--- a/Class.Show.html
+++ b/Class.Show.html
@@ -1,5 +1,5 @@
 
-Class.ShowSource code on Github
{-# OPTIONS --without-K #-}
+Class.ShowSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Show where
 
 open import Class.Show.Core public
diff --git a/Class.Traversable.Core.html b/Class.Traversable.Core.html
index b162842..bf6a61b 100644
--- a/Class.Traversable.Core.html
+++ b/Class.Traversable.Core.html
@@ -1,5 +1,5 @@
 
-Class.Traversable.CoreSource code on Github
{-# OPTIONS --without-K #-}
+Class.Traversable.CoreSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Traversable.Core where
 
 open import Class.Prelude
diff --git a/Class.Traversable.Instances.html b/Class.Traversable.Instances.html
index 512a1fe..d2e90ee 100644
--- a/Class.Traversable.Instances.html
+++ b/Class.Traversable.Instances.html
@@ -1,5 +1,5 @@
 
-Class.Traversable.InstancesSource code on Github
{-# OPTIONS --without-K #-}
+Class.Traversable.InstancesSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Traversable.Instances where
 
 open import Class.Prelude
diff --git a/Class.Traversable.html b/Class.Traversable.html
index 512977a..d5d32c1 100644
--- a/Class.Traversable.html
+++ b/Class.Traversable.html
@@ -1,5 +1,5 @@
 
-Class.TraversableSource code on Github
{-# OPTIONS --without-K #-}
+Class.TraversableSource code on Github
{-# OPTIONS --without-K #-}
 module Class.Traversable where
 
 open import Class.Traversable.Core public
diff --git a/Data.Bool.Base.html b/Data.Bool.Base.html
index bd981b2..e575d88 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 703a8d3..ddefcbd 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 9506248..9605100 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 8ae7b91..4f6ed22 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 67798fb..aeb145c 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 1640e3e..8ac3d85 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 cf31161..aa1e094 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.Container.Core.html b/Data.Container.Core.html
index df92b49..5ad9260 100644
--- a/Data.Container.Core.html
+++ b/Data.Container.Core.html
@@ -1,5 +1,5 @@
 
-Data.Container.CoreSource code on Github
------------------------------------------------------------------------
+Data.Container.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Containers core
diff --git a/Data.Container.Membership.html b/Data.Container.Membership.html
index a60e5e1..13373dc 100644
--- a/Data.Container.Membership.html
+++ b/Data.Container.Membership.html
@@ -1,5 +1,5 @@
 
-Data.Container.MembershipSource code on Github
------------------------------------------------------------------------
+Data.Container.MembershipSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Membership for containers
diff --git a/Data.Container.Morphism.Properties.html b/Data.Container.Morphism.Properties.html
index 5b15373..733690f 100644
--- a/Data.Container.Morphism.Properties.html
+++ b/Data.Container.Morphism.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Container.Morphism.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Container.Morphism.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Propertiers of any for containers
diff --git a/Data.Container.Morphism.html b/Data.Container.Morphism.html
index 0098a66..3e92383 100644
--- a/Data.Container.Morphism.html
+++ b/Data.Container.Morphism.html
@@ -1,5 +1,5 @@
 
-Data.Container.MorphismSource code on Github
------------------------------------------------------------------------
+Data.Container.MorphismSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Container Morphisms
diff --git a/Data.Container.Properties.html b/Data.Container.Properties.html
index 3b2bdc9..95b4f84 100644
--- a/Data.Container.Properties.html
+++ b/Data.Container.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Container.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Container.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of operations on containers
diff --git a/Data.Container.Related.html b/Data.Container.Related.html
index 838d7cf..4a0c740 100644
--- a/Data.Container.Related.html
+++ b/Data.Container.Related.html
@@ -1,5 +1,5 @@
 
-Data.Container.RelatedSource code on Github
------------------------------------------------------------------------
+Data.Container.RelatedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Several kinds of "relatedness" for containers such as equivalences,
diff --git a/Data.Container.Relation.Binary.Equality.Setoid.html b/Data.Container.Relation.Binary.Equality.Setoid.html
index 8f01106..75e3590 100644
--- a/Data.Container.Relation.Binary.Equality.Setoid.html
+++ b/Data.Container.Relation.Binary.Equality.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.Container.Relation.Binary.Equality.SetoidSource code on Github
------------------------------------------------------------------------
+Data.Container.Relation.Binary.Equality.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Equality over container extensions parametrised by some setoid
diff --git a/Data.Container.Relation.Binary.Pointwise.Properties.html b/Data.Container.Relation.Binary.Pointwise.Properties.html
index 5a5f334..6a2021c 100644
--- a/Data.Container.Relation.Binary.Pointwise.Properties.html
+++ b/Data.Container.Relation.Binary.Pointwise.Properties.html
@@ -1,5 +1,5 @@
 
-Data.Container.Relation.Binary.Pointwise.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.Container.Relation.Binary.Pointwise.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of pointwise equality for containers
diff --git a/Data.Container.Relation.Binary.Pointwise.html b/Data.Container.Relation.Binary.Pointwise.html
index df37ec4..ad56fb7 100644
--- a/Data.Container.Relation.Binary.Pointwise.html
+++ b/Data.Container.Relation.Binary.Pointwise.html
@@ -1,5 +1,5 @@
 
-Data.Container.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
+Data.Container.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise equality for containers
diff --git a/Data.Container.Relation.Unary.All.html b/Data.Container.Relation.Unary.All.html
index e73a8a6..62722bb 100644
--- a/Data.Container.Relation.Unary.All.html
+++ b/Data.Container.Relation.Unary.All.html
@@ -1,5 +1,5 @@
 
-Data.Container.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
+Data.Container.Relation.Unary.AllSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- All (□) for containers
diff --git a/Data.Container.Relation.Unary.Any.html b/Data.Container.Relation.Unary.Any.html
index c2e0025..a1377c5 100644
--- a/Data.Container.Relation.Unary.Any.html
+++ b/Data.Container.Relation.Unary.Any.html
@@ -1,5 +1,5 @@
 
-Data.Container.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
+Data.Container.Relation.Unary.AnySource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Any (◇) for containers
diff --git a/Data.Container.html b/Data.Container.html
index c0abc81..4dc40ce 100644
--- a/Data.Container.html
+++ b/Data.Container.html
@@ -1,5 +1,5 @@
 
-Data.ContainerSource code on Github
------------------------------------------------------------------------
+Data.ContainerSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Containers, based on the work of Abbott and others
diff --git a/Data.Digit.html b/Data.Digit.html
index 5291a76..bea41f1 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 add088c..8df87e0 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 5e38593..35d8ca0 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 cafa52f..365135c 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 31f8f18..eeaf17d 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 b7d1791..5c85ab8 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 0def0de..6060811 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 9f1db85..461ce7c 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 728f8cd..17ff5f6 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 9a22007..0f576bf 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 5ad51b8..12204b5 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 d2b0cf5..038c5d2 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 4e153d2..72c2e53 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 369caa0..511acb1 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 92cb6ae..91c2651 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 052951d..df131f5 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 3757e8d..af3b59e 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 f845deb..1a89df5 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 75cb0b1..e6fc57a 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 32bc829..c37bff5 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 08658be..2b9b7f0 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 8abf465..bfebc50 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 03d7151..dca6a3f 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 0422c06..940ad25 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 b65398e..fc968be 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 4e5f63e..d46ff75 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 20485c0..43335ae 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 cca835d..b4a179b 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 bb9e844..1ed19c6 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 aaffa76..4bd90c1 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 e893a66..e682621 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 e4e59cf..46db4f1 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 12f4759..fe1993e 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 89ebe13..3e17db8 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 321b1b7..4b43789 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 b78b94c..1c891bc 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 2e04816..97f2690 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 41d06a2..6e55e10 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 e74d7d7..777dcad 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.Permutation.Propositional.Properties.html b/Data.List.Relation.Binary.Permutation.Propositional.Properties.html
index b68b1b4..9e5912a 100644
--- a/Data.List.Relation.Binary.Permutation.Propositional.Properties.html
+++ b/Data.List.Relation.Binary.Permutation.Propositional.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Permutation.Propositional.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Permutation.Propositional.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of permutation
diff --git a/Data.List.Relation.Binary.Permutation.Propositional.html b/Data.List.Relation.Binary.Permutation.Propositional.html
index da9a68b..bfb576e 100644
--- a/Data.List.Relation.Binary.Permutation.Propositional.html
+++ b/Data.List.Relation.Binary.Permutation.Propositional.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Permutation.PropositionalSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Permutation.PropositionalSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An inductive definition for the permutation relation
diff --git a/Data.List.Relation.Binary.Pointwise.Base.html b/Data.List.Relation.Binary.Pointwise.Base.html
index 0a445db..cb375d2 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 83c23d3..60a08a3 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 fd51c68..2d66e4d 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.Sublist.Heterogeneous.Core.html b/Data.List.Relation.Binary.Sublist.Heterogeneous.Core.html
index ded5a34..56cf24a 100644
--- a/Data.List.Relation.Binary.Sublist.Heterogeneous.Core.html
+++ b/Data.List.Relation.Binary.Sublist.Heterogeneous.Core.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Sublist.Heterogeneous.CoreSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Sublist.Heterogeneous.CoreSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- This file contains some core definitions which are re-exported by
diff --git a/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html b/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
index d980f44..2fc6b9a 100644
--- a/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
+++ b/Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Sublist.Heterogeneous.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Sublist.Heterogeneous.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of the heterogeneous sublist relation
diff --git a/Data.List.Relation.Binary.Sublist.Heterogeneous.html b/Data.List.Relation.Binary.Sublist.Heterogeneous.html
index 6648b3b..0723f0f 100644
--- a/Data.List.Relation.Binary.Sublist.Heterogeneous.html
+++ b/Data.List.Relation.Binary.Sublist.Heterogeneous.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Sublist.HeterogeneousSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Sublist.HeterogeneousSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An inductive definition of the heterogeneous sublist relation
diff --git a/Data.List.Relation.Binary.Sublist.Setoid.Properties.html b/Data.List.Relation.Binary.Sublist.Setoid.Properties.html
index 7343111..a79b9f5 100644
--- a/Data.List.Relation.Binary.Sublist.Setoid.Properties.html
+++ b/Data.List.Relation.Binary.Sublist.Setoid.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Sublist.Setoid.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Sublist.Setoid.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties of the setoid sublist relation
diff --git a/Data.List.Relation.Binary.Sublist.Setoid.html b/Data.List.Relation.Binary.Sublist.Setoid.html
index e50290f..ae246d9 100644
--- a/Data.List.Relation.Binary.Sublist.Setoid.html
+++ b/Data.List.Relation.Binary.Sublist.Setoid.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Binary.Sublist.SetoidSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Binary.Sublist.SetoidSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An inductive definition of the sublist relation with respect to a
diff --git a/Data.List.Relation.Binary.Subset.Propositional.html b/Data.List.Relation.Binary.Subset.Propositional.html
index 12e5579..2b657f1 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 d2d4a60..70baf80 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 91ad429..347f2fb 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 4dc1634..51549e6 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 4197e60..15ae135 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.Properties.html b/Data.List.Relation.Unary.AllPairs.Properties.html
index 769e0c1..3d176bd 100644
--- a/Data.List.Relation.Unary.AllPairs.Properties.html
+++ b/Data.List.Relation.Unary.AllPairs.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.AllPairs.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.AllPairs.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to AllPairs
diff --git a/Data.List.Relation.Unary.AllPairs.html b/Data.List.Relation.Unary.AllPairs.html
index 8dd4b41..2277941 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 7f08548..c3622a1 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 8a9604f..45c8d3e 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.Linked.Properties.html b/Data.List.Relation.Unary.Linked.Properties.html
index eae89b2..efbb48e 100644
--- a/Data.List.Relation.Unary.Linked.Properties.html
+++ b/Data.List.Relation.Unary.Linked.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.Linked.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.Linked.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to Linked
diff --git a/Data.List.Relation.Unary.Linked.html b/Data.List.Relation.Unary.Linked.html
index 357c77e..1b2e8c4 100644
--- a/Data.List.Relation.Unary.Linked.html
+++ b/Data.List.Relation.Unary.Linked.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.LinkedSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.LinkedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lists where every consecutative pair of elements is related.
diff --git a/Data.List.Relation.Unary.Sorted.TotalOrder.Properties.html b/Data.List.Relation.Unary.Sorted.TotalOrder.Properties.html
index 5629ed9..796f97e 100644
--- a/Data.List.Relation.Unary.Sorted.TotalOrder.Properties.html
+++ b/Data.List.Relation.Unary.Sorted.TotalOrder.Properties.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.Sorted.TotalOrder.PropertiesSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.Sorted.TotalOrder.PropertiesSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sorted lists
diff --git a/Data.List.Relation.Unary.Sorted.TotalOrder.html b/Data.List.Relation.Unary.Sorted.TotalOrder.html
index 046a8c4..2008f2d 100644
--- a/Data.List.Relation.Unary.Sorted.TotalOrder.html
+++ b/Data.List.Relation.Unary.Sorted.TotalOrder.html
@@ -1,5 +1,5 @@
 
-Data.List.Relation.Unary.Sorted.TotalOrderSource code on Github
------------------------------------------------------------------------
+Data.List.Relation.Unary.Sorted.TotalOrderSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Sorted lists
diff --git a/Data.List.Relation.Unary.Unique.Setoid.html b/Data.List.Relation.Unary.Unique.Setoid.html
index d33c1ba..511e221 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 a72b61d..141c0cb 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.Sort.Base.html b/Data.List.Sort.Base.html
index 0376288..64ad6b9 100644
--- a/Data.List.Sort.Base.html
+++ b/Data.List.Sort.Base.html
@@ -1,5 +1,5 @@
 
-Data.List.Sort.BaseSource code on Github
------------------------------------------------------------------------
+Data.List.Sort.BaseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- The core definition of a sorting algorithm
diff --git a/Data.List.Sort.MergeSort.html b/Data.List.Sort.MergeSort.html
index af62aca..f3b0956 100644
--- a/Data.List.Sort.MergeSort.html
+++ b/Data.List.Sort.MergeSort.html
@@ -1,5 +1,5 @@
 
-Data.List.Sort.MergeSortSource code on Github
------------------------------------------------------------------------
+Data.List.Sort.MergeSortSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- An implementation of merge sort along with proofs of correctness.
diff --git a/Data.List.Sort.html b/Data.List.Sort.html
index e4789a3..53f8432 100644
--- a/Data.List.Sort.html
+++ b/Data.List.Sort.html
@@ -1,5 +1,5 @@
 
-Data.List.SortSource code on Github
------------------------------------------------------------------------
+Data.List.SortSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Functions and definitions for sorting lists
diff --git a/Data.List.html b/Data.List.html
index a72b084..b5adb97 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 a96996c..dbef328 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 1afc1de..c4e6056 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 cd905b5..69533c2 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.Binary.Connected.html b/Data.Maybe.Relation.Binary.Connected.html
index 3eeadc9..2a52536 100644
--- a/Data.Maybe.Relation.Binary.Connected.html
+++ b/Data.Maybe.Relation.Binary.Connected.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.Relation.Binary.ConnectedSource code on Github
------------------------------------------------------------------------
+Data.Maybe.Relation.Binary.ConnectedSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Lifting a relation such that `nothing` is also related to `just`
diff --git a/Data.Maybe.Relation.Binary.Pointwise.html b/Data.Maybe.Relation.Binary.Pointwise.html
index b31b78e..b8acc22 100644
--- a/Data.Maybe.Relation.Binary.Pointwise.html
+++ b/Data.Maybe.Relation.Binary.Pointwise.html
@@ -1,5 +1,5 @@
 
-Data.Maybe.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
+Data.Maybe.Relation.Binary.PointwiseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Pointwise lifting of relations to maybes
diff --git a/Data.Maybe.Relation.Unary.All.html b/Data.Maybe.Relation.Unary.All.html
index 9265d24..ce0ffa3 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 71872cd..93667f8 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 5cfae02..534fe21 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 22cd148..4dde785 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.Coprimality.html b/Data.Nat.Coprimality.html
index a22be2a..ed1c34c 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 a4226f4..b3224fb 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 fb94288..96d0536 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 cefb579..9b35f8a 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 cbe6ac4..d9ed6f1 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 d93960b..d24b4ba 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 edb5f09..75848dd 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 d0429e6..500ba12 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 23bbddf..080f040 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 ef4bb87..14a2146 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 cbc06d5..73f3e5d 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 3491ac5..23be3ed 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.html b/Data.Nat.html
index e5276e6..887470a 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 fa7e05f..52a4af6 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 306e58a..5afc677 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 2a538d9..7492da2 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 635b5f2..e3cd0dd 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 a792efb..14cc8d0 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 9e472d3..c6fdc75 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 eee41fe..17a4f78 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 afd4bfa..a25d747 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 82ce3db..e52eb72 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 eb53b71..8f0b2c9 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 1a65fad..29394b9 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 9cfbe27..d2d034f 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 c880c92..b8a2be1 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 828792d..280baa1 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 764733d..075e426 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 9ea88c5..dc6efa9 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.Record.html b/Data.Record.html
index 2507d6a..d8cff9c 100644
--- a/Data.Record.html
+++ b/Data.Record.html
@@ -1,5 +1,5 @@
 
-Data.RecordSource code on Github
------------------------------------------------------------------------
+Data.RecordSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Record types with manifest fields and "with", based on Randy
diff --git a/Data.Refinement.html b/Data.Refinement.html
index e7813ac..2d6b7e5 100644
--- a/Data.Refinement.html
+++ b/Data.Refinement.html
@@ -1,5 +1,5 @@
 
-Data.RefinementSource code on Github
------------------------------------------------------------------------
+Data.RefinementSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Refinement type: a value together with a proof irrelevant witness.
diff --git a/Data.Sign.Base.html b/Data.Sign.Base.html
index 0ed8931..c003481 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 76e058d..e35fa56 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 8565c82..c7ca015 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 93daebf..22c8656 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 b07ef07..f12b229 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 ff9fe45..b5deffc 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 b78cc2e..07b86d6 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 bd1da3b..3bd38e3 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 0e60e10..9aef30d 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 d96d207..1f33cb5 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 55dc2e7..9e154a5 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 a57ab7b..766d18c 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 af0bb6f..38d1f5a 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.html b/Data.Sum.html
index 8f4bc14..f5e5c44 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 351d233..d7cd5d5 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 1588eff..de62d1c 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 916485a..d8f618d 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 92fc1af..d8aa74d 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 da809b1..09ae58f 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 9373162..0097d5a 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 90204a5..b74bd87 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 a01fe8c..f7cce12 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 84ea71e..72acc06 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.Universe.html b/Data.Universe.html
index de5b4e3..0f6b187 100644
--- a/Data.Universe.html
+++ b/Data.Universe.html
@@ -1,5 +1,5 @@
 
-Data.UniverseSource code on Github
------------------------------------------------------------------------
+Data.UniverseSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Universes
diff --git a/Data.Vec.Base.html b/Data.Vec.Base.html
index f3470ca..5e61b3f 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 2265c6d..2110169 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 f3562e2..bbc0cd5 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.N-ary.html b/Data.Vec.N-ary.html
index a855612..54943e9 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 ccbe589..d77a309 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 5c8d838..144ae91 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.html b/Data.Vec.html
index c7de7e6..6465113 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.W.html b/Data.W.html
index 5455011..9449fa6 100644
--- a/Data.W.html
+++ b/Data.W.html
@@ -1,5 +1,5 @@
 
-Data.WSource code on Github
------------------------------------------------------------------------
+Data.WSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- W-types
diff --git a/Data.Word64.Base.html b/Data.Word64.Base.html
index efb6d92..3577a8e 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 3fdef4e..81f9f92 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/Data.Word64.html b/Data.Word64.html
index a5c1fc2..0aa97e2 100644
--- a/Data.Word64.html
+++ b/Data.Word64.html
@@ -1,5 +1,5 @@
 
-Data.Word64Source code on Github
------------------------------------------------------------------------
+Data.Word64Source code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Machine words
diff --git a/Effect.Applicative.html b/Effect.Applicative.html
index ab916d3..b4191c0 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 6d0f021..4096ac8 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 4b78aa5..2bbb0ee 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 759ae67..dc91990 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 c4f8b0a..cf0943c 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 bf4e4a2..a40d281 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 872e737..d561b0f 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 4ec7e9f..2bc64a7 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 9b93d4a..c7257bd 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 5e32762..49a0759 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 bfc5de2..bbcadb2 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 40b4514..36f8429 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 11a7778..04fe459 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 4aaa0f9..1e9e308 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 7c60be7..9281ba2 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 b86c07c..b8120b3 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 3be505f..9711752 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 86635c4..c549902 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 6d60608..ed417bd 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 02c1342..30a5347 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 d73b509..77eaa89 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 395c1dd..f5e4eb8 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 eca811a..85992ab 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 f36b501..ce65889 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 d660487..69059b8 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 2d791de..8b4e072 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 7b3c4f3..7168270 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 6f20caa..efc0c77 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 98e946f..d3e5fd6 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 ef4811e..ae4e1b0 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 bcad6d4..22caf2a 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 e3947b6..9961dc4 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 4d8a5e9..27f51e5 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 d407603..ecf0835 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 cd49a3a..dd07936 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 8fe4710..a653f51 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 ea9916f..0e8f070 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 15ed54e..bb86d2f 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 a751080..8812bc3 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 6136472..24fc118 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 9dbf3e5..f830ed2 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 3e587e5..24fe125 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 982f797..8d64480 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/Meta.Init.html b/Meta.Init.html
index 7b9b798..3cb16da 100644
--- a/Meta.Init.html
+++ b/Meta.Init.html
@@ -1,5 +1,5 @@
 
-Meta.InitSource code on Github
{-# OPTIONS --safe --without-K #-}
+Meta.InitSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Meta.Init where
 
diff --git a/Meta.Prelude.html b/Meta.Prelude.html
index 8d813e2..83ed0c2 100644
--- a/Meta.Prelude.html
+++ b/Meta.Prelude.html
@@ -1,5 +1,5 @@
 
-Meta.PreludeSource code on Github
{-# OPTIONS --safe --without-K #-}
+Meta.PreludeSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Meta.Prelude where
 
diff --git a/Reflection.AST.Abstraction.html b/Reflection.AST.Abstraction.html
index d8ab6ef..98b1c99 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 77a092b..cd0eee5 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 c5b0426..1592cfe 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 763d71b..882d8a5 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 309e21f..60a2d0d 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 c2b2fa2..1bb492b 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 f691a3c..e293826 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 64526a7..a428210 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 32c0f28..d3517f2 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 9aac77e..26f01a9 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 a6f7bde..285e4fa 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 a79acf2..9d0cc0f 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 92cf443..a95e306 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 cf41c88..62b2cf7 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 96bce9b..adcae47 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.AlphaEquality.html b/Reflection.AlphaEquality.html
index 9fdba5c..d0301b2 100644
--- a/Reflection.AlphaEquality.html
+++ b/Reflection.AlphaEquality.html
@@ -1,5 +1,5 @@
 
-Reflection.AlphaEqualitySource code on Github
------------------------------------------------------------------------
+Reflection.AlphaEqualitySource code on Github
------------------------------------------------------------------------
 -- Alpha equality
 --
 -- Taken almost verbatim from the Agda stdlib
diff --git a/Reflection.AntiUnification.html b/Reflection.AntiUnification.html
index fd13fe7..dd6941f 100644
--- a/Reflection.AntiUnification.html
+++ b/Reflection.AntiUnification.html
@@ -1,5 +1,5 @@
 
-Reflection.AntiUnificationSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.AntiUnificationSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 ----------------------------------------------------------------------
 -- Anti-Unification
diff --git a/Reflection.Debug.html b/Reflection.Debug.html
index 734d506..8be1888 100644
--- a/Reflection.Debug.html
+++ b/Reflection.Debug.html
@@ -1,5 +1,5 @@
 
-Reflection.DebugSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.DebugSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Reflection.Debug where
 
diff --git a/Reflection.Syntax.html b/Reflection.Syntax.html
index 009ca85..c07067f 100644
--- a/Reflection.Syntax.html
+++ b/Reflection.Syntax.html
@@ -1,5 +1,5 @@
 
-Reflection.SyntaxSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.SyntaxSource code on Github
{-# OPTIONS --safe --without-K #-}
 
 module Reflection.Syntax where
 
diff --git a/Reflection.TCI.html b/Reflection.TCI.html
index da55830..3d3b88a 100644
--- a/Reflection.TCI.html
+++ b/Reflection.TCI.html
@@ -1,5 +1,5 @@
 
-Reflection.TCISource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.TCISource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- Improved TC
 --------------------------------------------------------------------------------
diff --git a/Reflection.TCM.Format.html b/Reflection.TCM.Format.html
index 9617e67..7a0aa13 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 6ed6412..34e8191 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 fe7c836..315244a 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.Tactic.html b/Reflection.Tactic.html
index eb87ace..3ac577d 100644
--- a/Reflection.Tactic.html
+++ b/Reflection.Tactic.html
@@ -1,5 +1,5 @@
 
-Reflection.TacticSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.TacticSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- Types & functions for interacting with tactics/metaprograms
 --------------------------------------------------------------------------------
diff --git a/Reflection.Utils.Debug.html b/Reflection.Utils.Debug.html
index e466b75..145515a 100644
--- a/Reflection.Utils.Debug.html
+++ b/Reflection.Utils.Debug.html
@@ -1,5 +1,5 @@
 
-Reflection.Utils.DebugSource code on Github
-------------------------------------------------
+Reflection.Utils.DebugSource code on Github
-------------------------------------------------
 -- ** Errors, debugging
 
 {-# OPTIONS --safe --without-K #-}
diff --git a/Reflection.Utils.TCI.html b/Reflection.Utils.TCI.html
index 92d98ba..77d28c9 100644
--- a/Reflection.Utils.TCI.html
+++ b/Reflection.Utils.TCI.html
@@ -1,5 +1,5 @@
 
-Reflection.Utils.TCISource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.Utils.TCISource code on Github
{-# OPTIONS --safe --without-K #-}
 
 open import Meta.Prelude
 open import Meta.Init
diff --git a/Reflection.Utils.TCM.html b/Reflection.Utils.TCM.html
index 698c00c..4baea20 100644
--- a/Reflection.Utils.TCM.html
+++ b/Reflection.Utils.TCM.html
@@ -1,5 +1,5 @@
 
-Reflection.Utils.TCMSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.Utils.TCMSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Reflection.Utils.TCM where
 
 open import Reflection
diff --git a/Reflection.Utils.html b/Reflection.Utils.html
index 99591ad..90b6693 100644
--- a/Reflection.Utils.html
+++ b/Reflection.Utils.html
@@ -1,5 +1,5 @@
 
-Reflection.UtilsSource code on Github
{-# OPTIONS --safe --without-K #-}
+Reflection.UtilsSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Reflection.Utils where
 
 open import Meta.Prelude
diff --git a/Reflection.html b/Reflection.html
index 9c4bf13..aeb1e17 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 ae332d8..f9a82d5 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 0da8c58..2ee3cc0 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 d74fb1d..d4ec7cf 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 a0ced5e..e485c05 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 9a64dc9..682c19f 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 0de9ee3..cffd60c 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 e3b20ca..6eb440b 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 f000327..c28ef22 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 41a2e8c..9b3a2c9 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 0a74adb..40c9fbe 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 78ad24a..7f55dc4 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.Subst.Equality.html b/Relation.Binary.Construct.Subst.Equality.html
index e60ffa6..a6df890 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 80c3625..e58170c 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 e0db84a..ec0f47d 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 3529d17..e80251d 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 4ee62a7..bc1b6b2 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 32e35f9..78d939f 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 5a8d3f2..7962e5c 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 7b65d03..2d63a2c 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 9979403..678744e 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 3b988ee..89a2e1a 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 72127a3..72faaa2 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 2dc547c..f54a8e9 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 885f839..f50ceac 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 5887c3e..6607362 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 d7a0109..5f2b7c3 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 e073e96..c3b7042 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 2fc9f55..3b6c4d5 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 2a42b18..9416c1a 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 16ad2d1..e97a96f 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 1587a3f..d57dc98 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 98a68c8..412f2f0 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 c447ef6..17f4a46 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 2020527..a0cf03f 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 123d4ad..0deb325 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 3a10bea..cc5a1eb 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 f0bd346..3b8e771 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 a23b4e2..100d48a 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 e2f9b1e..1cec7ac 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 9c36451..0d8746b 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 c6f9cfd..9da4a1a 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 f1207f6..c017361 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 f4a4a88..2115f77 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 e32e506..ea64bfb 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 f37bca8..f62a658 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 9822a0e..a7b0f26 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 fb9501a..df84107 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 a439077..c0bbaa3 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 6c1c2ad..e1423ed 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 8848756..8cbf363 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 0e48cb3..49456d0 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 0fdb1d9..136afc5 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 f919ae3..d350d40 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 10fdecd..4cd4b8a 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 e969d9e..8d2b0bf 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 513f085..73137e9 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 f878116..246d50a 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 726f84a..ba178e5 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 cd964c2..2aa28ed 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 8f1575a..32a55ee 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 2688cfc..e036e27 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 7f9343f..8a43b85 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/Tactic.AnyOf.html b/Tactic.AnyOf.html
index cf97f2d..b3753e1 100644
--- a/Tactic.AnyOf.html
+++ b/Tactic.AnyOf.html
@@ -1,5 +1,5 @@
 
-Tactic.AnyOfSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.AnyOfSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- anyOf: take the first term that type checks
 --------------------------------------------------------------------------------
diff --git a/Tactic.Assumption.html b/Tactic.Assumption.html
index f90659b..db4defc 100644
--- a/Tactic.Assumption.html
+++ b/Tactic.Assumption.html
@@ -1,5 +1,5 @@
 
-Tactic.AssumptionSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.AssumptionSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- assumption: try to solve the goal with one of the available assumptions
 --------------------------------------------------------------------------------
diff --git a/Tactic.ByEq.html b/Tactic.ByEq.html
index 6d61924..b88b4f7 100644
--- a/Tactic.ByEq.html
+++ b/Tactic.ByEq.html
@@ -1,5 +1,5 @@
 
-Tactic.ByEqSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.ByEqSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Tactic.ByEq where
 
 open import Meta.Init hiding (TC)
diff --git a/Tactic.Case.html b/Tactic.Case.html
index 789471a..f3447b0 100644
--- a/Tactic.Case.html
+++ b/Tactic.Case.html
@@ -1,5 +1,5 @@
 
-Tactic.CaseSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.CaseSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- case: pattern-match on the first term, continue with the second tactic
 --------------------------------------------------------------------------------
diff --git a/Tactic.ClauseBuilder.html b/Tactic.ClauseBuilder.html
index 66fc21c..d4cf4f3 100644
--- a/Tactic.ClauseBuilder.html
+++ b/Tactic.ClauseBuilder.html
@@ -1,5 +1,5 @@
 
-Tactic.ClauseBuilderSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.ClauseBuilderSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Tactic.ClauseBuilder where
 
 open import Meta.Prelude hiding ([_,_])
diff --git a/Tactic.Constrs.html b/Tactic.Constrs.html
index 4e08ad7..4e09dfa 100644
--- a/Tactic.Constrs.html
+++ b/Tactic.Constrs.html
@@ -1,5 +1,5 @@
 
-Tactic.ConstrsSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.ConstrsSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- tryConstrs: Try to refine the goal with constructors recursively,
 -- applying some other tactic at the leaves
diff --git a/Tactic.Defaults.html b/Tactic.Defaults.html
index 1933b3c..0b9ac88 100644
--- a/Tactic.Defaults.html
+++ b/Tactic.Defaults.html
@@ -1,5 +1,5 @@
 
-Tactic.DefaultsSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.DefaultsSource code on Github
{-# OPTIONS --safe --without-K #-}
 module Tactic.Defaults where
 
 open import Meta.Prelude
diff --git a/Tactic.Derive.DecEq.html b/Tactic.Derive.DecEq.html
index e6d62d7..91503f1 100644
--- a/Tactic.Derive.DecEq.html
+++ b/Tactic.Derive.DecEq.html
@@ -1,5 +1,5 @@
 
-Tactic.Derive.DecEqSource code on Github
-- Deriving decidable equality. This works in several cases that use
+Tactic.Derive.DecEqSource code on Github
-- Deriving decidable equality. This works in several cases that use
 -- mutual recursion, examples are at the bottom.
 --
 -- TODO: This breaks with:
diff --git a/Tactic.Derive.Show.html b/Tactic.Derive.Show.html
index f7a465b..87138a8 100644
--- a/Tactic.Derive.Show.html
+++ b/Tactic.Derive.Show.html
@@ -1,5 +1,5 @@
 
-Tactic.Derive.ShowSource code on Github
-- Deriving show.
+Tactic.Derive.ShowSource code on Github
-- Deriving show.
 
 {-# OPTIONS -v allTactics:100 #-}
 {-# OPTIONS --safe #-}
diff --git a/Tactic.Derive.TestTypes.html b/Tactic.Derive.TestTypes.html
index d29dccd..74ef898 100644
--- a/Tactic.Derive.TestTypes.html
+++ b/Tactic.Derive.TestTypes.html
@@ -1,5 +1,5 @@
 
-Tactic.Derive.TestTypesSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.Derive.TestTypesSource code on Github
{-# OPTIONS --safe --without-K #-}
 {-# OPTIONS -v allTactics:100 #-}
 module Tactic.Derive.TestTypes where
 
diff --git a/Tactic.Derive.html b/Tactic.Derive.html
index 84e3257..ad9cc4c 100644
--- a/Tactic.Derive.html
+++ b/Tactic.Derive.html
@@ -1,5 +1,5 @@
 
-Tactic.DeriveSource code on Github
-- Generic type class dervations. Works with mutually recursive types
+Tactic.DeriveSource code on Github
-- Generic type class dervations. Works with mutually recursive types
 -- and can use mutual recursion to satisfy the termination
 -- checker. Writing an actual derivation strategy then does not
 -- require dealing with any mutual recursion, it is all handled here.
diff --git a/Tactic.EquationalReasoning.html b/Tactic.EquationalReasoning.html
index 270eb58..0df126e 100644
--- a/Tactic.EquationalReasoning.html
+++ b/Tactic.EquationalReasoning.html
@@ -1,5 +1,5 @@
 
-Tactic.EquationalReasoningSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.EquationalReasoningSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- equational reasoning that can use tactics at each step
 --------------------------------------------------------------------------------
diff --git a/Tactic.Eta.html b/Tactic.Eta.html
index 857f117..26870d5 100644
--- a/Tactic.Eta.html
+++ b/Tactic.Eta.html
@@ -1,5 +1,5 @@
 
-Tactic.EtaSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.EtaSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- eta: unify with an eta-expanded version of the argument
 --------------------------------------------------------------------------------
diff --git a/Tactic.Existentials.html b/Tactic.Existentials.html
index 6efed6b..9eaf13d 100644
--- a/Tactic.Existentials.html
+++ b/Tactic.Existentials.html
@@ -1,5 +1,5 @@
 
-Tactic.ExistentialsSource code on Github
module Tactic.Existentials where
+Tactic.ExistentialsSource code on Github
module Tactic.Existentials where
 
 open import Meta.Prelude
 
diff --git a/Tactic.Extra.html b/Tactic.Extra.html
index 2ed0dbc..bf4bc10 100644
--- a/Tactic.Extra.html
+++ b/Tactic.Extra.html
@@ -1,5 +1,5 @@
 
-Tactic.ExtraSource code on Github
{-# OPTIONS -v extra:100 #-}
+Tactic.ExtraSource code on Github
{-# OPTIONS -v extra:100 #-}
 module Tactic.Extra where
 
 open import Meta.Prelude
diff --git a/Tactic.Intro.html b/Tactic.Intro.html
index 61113dd..1b1cb52 100644
--- a/Tactic.Intro.html
+++ b/Tactic.Intro.html
@@ -1,5 +1,5 @@
 
-Tactic.IntroSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.IntroSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- intro, intros: introduce one or many variables & continue with another tactic
 --------------------------------------------------------------------------------
diff --git a/Tactic.MonoidSolver.html b/Tactic.MonoidSolver.html
index 37ddc47..1d1d865 100644
--- a/Tactic.MonoidSolver.html
+++ b/Tactic.MonoidSolver.html
@@ -1,5 +1,5 @@
 
-Tactic.MonoidSolverSource code on Github
------------------------------------------------------------------------
+Tactic.MonoidSolverSource code on Github
------------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Reflection-based solver for monoid equalities
diff --git a/Tactic.ReduceDec.html b/Tactic.ReduceDec.html
index e3eea50..5104c5e 100644
--- a/Tactic.ReduceDec.html
+++ b/Tactic.ReduceDec.html
@@ -1,5 +1,5 @@
 
-Tactic.ReduceDecSource code on Github
{-# OPTIONS --safe --without-K #-}
+Tactic.ReduceDecSource code on Github
{-# OPTIONS --safe --without-K #-}
 --------------------------------------------------------------------------------
 -- reduceDec: looks for proofs of P or ¬P to reduce ⌊ decP ⌋
 --------------------------------------------------------------------------------
diff --git a/Tactic.Rewrite.html b/Tactic.Rewrite.html
index a4c1094..f30715f 100644
--- a/Tactic.Rewrite.html
+++ b/Tactic.Rewrite.html
@@ -1,5 +1,5 @@
 
-Tactic.RewriteSource code on Github
{-# OPTIONS -v rewrite:100 #-}
+Tactic.RewriteSource code on Github
{-# OPTIONS -v rewrite:100 #-}
 module Tactic.Rewrite where
 
 open import Meta.Prelude hiding (_^_)
diff --git a/Tactic.Try.html b/Tactic.Try.html
index a5556d7..2c81cea 100644
--- a/Tactic.Try.html
+++ b/Tactic.Try.html
@@ -1,5 +1,5 @@
 
-Tactic.TrySource code on Github
{-# OPTIONS -v try:100 #-}
+Tactic.TrySource code on Github
{-# OPTIONS -v try:100 #-}
 module Tactic.Try where
 
 open import Meta.Prelude
diff --git a/Tactic.html b/Tactic.html
index 3e76d6a..14a345e 100644
--- a/Tactic.html
+++ b/Tactic.html
@@ -1,5 +1,5 @@
 
-TacticSource code on Github
module Tactic where
+TacticSource code on Github
module Tactic where
 
 open import Tactic.Try public
 open import Tactic.Rewrite public
diff --git a/Text.Format.Generic.html b/Text.Format.Generic.html
index e2b419f..7564dc7 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 d9eafd5..4fbdf29 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 0aa7ad5..b00d9d0 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 ef14fe7..54ace05 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 79d0820..3dccbfc 100644
--- a/index.html
+++ b/index.html
@@ -1,5 +1,5 @@
 
-standard-library-metaSource code on Github
module standard-library-meta where
+standard-library-metaSource code on Github
module standard-library-meta where
 
 open import Algebra.Function
 
diff --git a/standard-library-meta.html b/standard-library-meta.html
index 3310d36..ce5d9ed 100644
--- a/standard-library-meta.html
+++ b/standard-library-meta.html
@@ -1,5 +1,5 @@
 
-standard-library-metaSource code on Github
module standard-library-meta where
+standard-library-metaSource code on Github
module standard-library-meta where
 
 open import Algebra.Function
 
diff --git a/typecheck.time b/typecheck.time
index 3d81c9e..8241a8b 100644
--- a/typecheck.time
+++ b/typecheck.time
@@ -1,41 +1,41 @@
-TOTAL: 3m22s
-Algebra/Function: 0m10s
-Meta/Prelude: 1m18s
-Class/MonadError: 0m47s
+TOTAL: 3m40s
+Algebra/Function: 0m11s
+Meta/Prelude: 1m24s
+Class/MonadError: 0m52s
 Class/MonadReader: 0m0s
-Reflection/Syntax: 0m0s
+Reflection/Syntax: 0m1s
 Reflection/Debug: 0m0s
 Class/MonadTC: 0m1s
-Reflection/TCI: 0m1s
+Reflection/TCI: 0m0s
 Meta/Init: 0m0s
 Reflection/Tactic: 0m0s
-Reflection/Utils: 0m0s
+Reflection/Utils: 0m1s
 Reflection/Utils/Debug: 0m1s
 Class/MonadError/Instances: 0m0s
 Class/MonadReader/Instances: 0m0s
 Class/MonadTC/Instances: 0m0s
-Reflection/Utils/TCI: 0m13s
+Reflection/Utils/TCI: 0m14s
 Reflection/Utils/TCM: 0m0s
-Reflection/AlphaEquality: 0m0s
+Reflection/AlphaEquality: 0m1s
 Reflection/AntiUnification: 0m0s
 Tactic/Try: 0m1s
-Tactic/Rewrite: 0m2s
-Tactic/Extra: 0m0s
+Tactic/Rewrite: 0m1s
+Tactic/Extra: 0m1s
 Tactic/Existentials: 0m0s
 Tactic/ByEq: 0m0s
-Tactic/AnyOf: 0m1s
+Tactic/AnyOf: 0m0s
 Tactic/Defaults: 0m0s
-Tactic/Assumption: 0m0s
-Tactic/ClauseBuilder: 0m31s
-Tactic/Case: 0m1s
-Tactic/Constrs: 0m0s
+Tactic/Assumption: 0m1s
+Tactic/ClauseBuilder: 0m33s
+Tactic/Case: 0m0s
+Tactic/Constrs: 0m1s
 Tactic/EquationalReasoning: 0m0s
-Tactic/Eta: 0m1s
-Tactic/Intro: 0m0s
+Tactic/Eta: 0m0s
+Tactic/Intro: 0m1s
 Tactic/ReduceDec: 0m1s
 Tactic/Derive: 0m0s
 Tactic/Derive/TestTypes: 0m2s
 Tactic/Derive/DecEq: 0m6s
-Tactic/Derive/Show: 0m2s
+Tactic/Derive/Show: 0m3s
 Tactic: 0m0s
 standard-library-meta: 0m0s