diff --git a/plutus-metatheory/src/Algorithmic.lagda.md b/plutus-metatheory/src/Algorithmic.lagda.md
index c2b7d68764a..f4a71a6dd4f 100644
--- a/plutus-metatheory/src/Algorithmic.lagda.md
+++ b/plutus-metatheory/src/Algorithmic.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic
+layout: page
+---
 ```
 module Algorithmic where
 ```
@@ -335,4 +339,4 @@ constr-cong' :  ∀{Γ : Ctx Φ}{n}{i : Fin n}{A : Vec (List (Φ ⊢Nf⋆ *)) n}
             → (q : subst (IList (Γ ⊢_)) p' cs' ≡ subst (IList (Γ ⊢_)) p cs)
             → constr i A p' cs' ≡ constr i A p cs
 constr-cong' refl refl refl = refl
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
index 1695a7f0041..7d4ab0e1ba8 100644
--- a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCK
+layout: page
+---
 # CK machine
 
 ```
diff --git a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
index ed4bd820b86..7a40b7f9f10 100644
--- a/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CKvsCEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.BehaviouralEquivalence.CCvsCEK
+layout: page
+---
 # CEK behavioural equivalence with CK machine
 
 ```
diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
index 3ab56f1c241..321dae4a290 100644
--- a/plutus-metatheory/src/Algorithmic/CEK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CEK
+layout: page
+---
 # CEK machine that discharges builtin args
 
 ```
diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md
index bf32c1c0710..83b627d7f77 100644
--- a/plutus-metatheory/src/Algorithmic/CK.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/CK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.CK
+layout: page
+---
 # CK machine
 
 ```
diff --git a/plutus-metatheory/src/Algorithmic/Completeness.lagda.md b/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
index deda4d82d20..fd0fa2affc2 100644
--- a/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Completeness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Completeness
+layout: page
+---
 ```
 module Algorithmic.Completeness where
 
diff --git a/plutus-metatheory/src/Algorithmic/Erasure.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
index c2638ef463d..9b658d1530a 100644
--- a/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Erasure.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure
+layout: page
+---
 ```
 {-# OPTIONS --injective-type-constructors #-}
 
diff --git a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
index 7eca7b9424c..c27e8d0dcbc 100644
--- a/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Erasure/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Erasure.RenamingSubstitution
+layout: page
+---
 ```
 module Algorithmic.Erasure.RenamingSubstitution where
 ```
diff --git a/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md b/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
index 410c7ab315b..2d4c5b558d3 100644
--- a/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Evaluation.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Evaluation
+layout: page
+---
 ```
 module Algorithmic.Evaluation where
 ```
@@ -85,4 +89,4 @@ stepper {A} t n with eval (gas n) t
 ... | steps x (error _)   = return (error A)
 
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Algorithmic/Examples.lagda.md b/plutus-metatheory/src/Algorithmic/Examples.lagda.md
index 08ccda7a4e8..113d5120720 100644
--- a/plutus-metatheory/src/Algorithmic/Examples.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Examples.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Examples
+layout: page
+---
 ```
 module Algorithmic.Examples where
 ```
diff --git a/plutus-metatheory/src/Algorithmic/Properties.lagda.md b/plutus-metatheory/src/Algorithmic/Properties.lagda.md
index 055df253906..97b390b2f80 100644
--- a/plutus-metatheory/src/Algorithmic/Properties.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Properties.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Properties
+layout: page
+---
 ```
 module Algorithmic.Properties where
 ```
diff --git a/plutus-metatheory/src/Algorithmic/Reduction.lagda.md b/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
index b07e1b9fbfc..2fed602dcca 100644
--- a/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Reduction.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Reduction
+layout: page
+---
 ```
 module Algorithmic.Reduction where
 ```
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
index 8f95dcaaab7..6a90b8e297f 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC
+layout: page
+---
 ```
 module Algorithmic.ReductionEC where
 ```
@@ -371,4 +375,4 @@ ival : ∀ b → Value (builtin b / refl)
 ival b = V-I b base
 -- -}
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
index feaef184d64..301f6b14217 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Determinism
+layout: page
+---
 ```
 module Algorithmic.ReductionEC.Determinism where
 ```
@@ -684,4 +688,4 @@ determinism {L = L} (ruleErr E' p) (ruleErr E'' q) | step ¬VL E err r' U with U
 ... | refl ,, refl ,, refl | refl ,, refl ,, refl = refl
 -- -}
 ```  
-    
\ No newline at end of file
+    
diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
index e726bb099a0..dd25415ce47 100644
--- a/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/ReductionEC/Progress.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.ReductionEC.Progress
+layout: page
+---
 ```
 module Algorithmic.ReductionEC.Progress where
 ```
@@ -139,4 +143,4 @@ progress (case M cases)  with progress M
 ... | step (ruleErr E refl) = step (ruleErr (case cases E) refl)
 ... | done (V-constr e Tss refl refl vs refl) = step (ruleEC [] (β-case e Tss refl vs refl cases) refl refl)
 
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
index a37eea391a1..02e1e9cd2b9 100644
--- a/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.RenamingSubstitution
+layout: page
+---
 ```
 module Algorithmic.RenamingSubstitution where
 ```
@@ -591,4 +595,4 @@ exts⋆ˢ : ∀{Φ}{Γ Δ : Ctx Φ}
 -}
 ```
 
-   
\ No newline at end of file
+   
diff --git a/plutus-metatheory/src/Algorithmic/Signature.lagda.md b/plutus-metatheory/src/Algorithmic/Signature.lagda.md
index 88eea3fbbc6..ad9cf4b9722 100644
--- a/plutus-metatheory/src/Algorithmic/Signature.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Signature.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Algorithmic.Signature
+layout: page
+---
 ```
 module Algorithmic.Signature where
 ```
@@ -94,4 +97,4 @@ uniqueSigTy (bresult _) (bresult _) = refl
 uniqueSigTy (A B⇒ s) (.A B⇒ s') = cong (A B⇒_) (uniqueSigTy s s')
 uniqueSigTy (sucΠ s) (sucΠ s') = cong sucΠ (uniqueSigTy s s') 
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Algorithmic/Soundness.lagda.md b/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
index 418e9d41778..46c8188e0ba 100644
--- a/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
+++ b/plutus-metatheory/src/Algorithmic/Soundness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Algorithmic.Soundness
+layout: page
+---
 ```
 module Algorithmic.Soundness where
 
diff --git a/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md b/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
index 39e0405604a..8e79bd8d526 100644
--- a/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
+++ b/plutus-metatheory/src/Builtin/Constant/AtomicType.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Builtin.Constant.AtomicType
+layout: page
+---
 
 ```
 module Builtin.Constant.AtomicType where
diff --git a/plutus-metatheory/src/Check.lagda.md b/plutus-metatheory/src/Check.lagda.md
index dce238100f4..eaad6869c60 100644
--- a/plutus-metatheory/src/Check.lagda.md
+++ b/plutus-metatheory/src/Check.lagda.md
@@ -1,4 +1,5 @@
 ---
+title: Type Checker
 layout: page
 ---
 ## Type checker
diff --git a/plutus-metatheory/src/Cost.lagda.md b/plutus-metatheory/src/Cost.lagda.md
index 9ecbcc525e7..6f0ceaa50be 100644
--- a/plutus-metatheory/src/Cost.lagda.md
+++ b/plutus-metatheory/src/Cost.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost
+layout: page
+---
 # Costs
 
 
diff --git a/plutus-metatheory/src/Cost/Base.lagda.md b/plutus-metatheory/src/Cost/Base.lagda.md
index 184f3d9b465..66a57678041 100644
--- a/plutus-metatheory/src/Cost/Base.lagda.md
+++ b/plutus-metatheory/src/Cost/Base.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Base
+layout: page
+---
 ```
 module Cost.Base where 
 
@@ -92,4 +95,4 @@ record MachineParameters (Cost : Set) : Set where
 
     startupCost : Cost 
     startupCost = cekMachineCost BStartup
-``` 
\ No newline at end of file
+``` 
diff --git a/plutus-metatheory/src/Cost/Model.lagda.md b/plutus-metatheory/src/Cost/Model.lagda.md
index 74cf58ce95e..4af0668ea3d 100644
--- a/plutus-metatheory/src/Cost/Model.lagda.md
+++ b/plutus-metatheory/src/Cost/Model.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Cost.Model
+layout: page
+---
 # Builtin Cost Models
 
 ```
diff --git a/plutus-metatheory/src/Cost/Raw.lagda.md b/plutus-metatheory/src/Cost/Raw.lagda.md
index b01d5ea183f..8c2074a957e 100644
--- a/plutus-metatheory/src/Cost/Raw.lagda.md
+++ b/plutus-metatheory/src/Cost/Raw.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Raw
+layout: page
+---
 # Raw Cost structures to inferface with Haskell
 
 ```
diff --git a/plutus-metatheory/src/Cost/Size.lagda.md b/plutus-metatheory/src/Cost/Size.lagda.md
index 0e1e33e9ce2..86776e130de 100644
--- a/plutus-metatheory/src/Cost/Size.lagda.md
+++ b/plutus-metatheory/src/Cost/Size.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Cost.Size
+layout: page
+---
 # Size of Constants
 
 ```
@@ -83,4 +87,4 @@ defaultConstantMeasure (tmCon (pair t u) (x , y)) =
 defaultValueMeasure : Value → CostingNat 
 defaultValueMeasure (V-con ty x) = defaultConstantMeasure (tmCon ty x)
 defaultValueMeasure _ = 0
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
index 7cc7104870a..e565fd65a0d 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/ChurchNat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: ChurchNat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.ChurchNat where
 ```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
index 83ab8ef832f..5b90ee636d0 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/Function.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Function
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Function where
 ```
diff --git a/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md b/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
index f27ad6cf27e..09e30eb0977 100644
--- a/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
+++ b/plutus-metatheory/src/Declarative/Examples/StdLib/Nat.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Nat
+layout: page
+---
 ```
 module Declarative.Examples.StdLib.Nat where
 ```
diff --git a/plutus-metatheory/src/Evaluator/Base.lagda.md b/plutus-metatheory/src/Evaluator/Base.lagda.md
index ab12c3e9e54..522661916ec 100644
--- a/plutus-metatheory/src/Evaluator/Base.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Base.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Base
+layout: page
+---
 ```
 module Evaluator.Base where 
 
@@ -104,4 +107,4 @@ reportError (runtimeError runtimeTypeError) = "runtimeTypeError"
 ```
 maxsteps : Nat
 maxsteps = 10000000000
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Evaluator/Program.lagda.md b/plutus-metatheory/src/Evaluator/Program.lagda.md
index f289e8beba9..2c6d8c5b28f 100644
--- a/plutus-metatheory/src/Evaluator/Program.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Program.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Program Evaluators
+layout: page
+---
 # Evaluators for Programs
 
 ```
@@ -227,4 +231,4 @@ typeCheckProgramN namedprog = do
  -}
   return (prettyPrintTy (unshifterTy Z (extricateScopeTy (extricateNf⋆ A))))
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Evaluator/Term.lagda.md b/plutus-metatheory/src/Evaluator/Term.lagda.md
index 254f15d906d..526705ed553 100644
--- a/plutus-metatheory/src/Evaluator/Term.lagda.md
+++ b/plutus-metatheory/src/Evaluator/Term.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Term - Haskell Interface to the Metatheory
+layout: page
+---
 # Haskell Interface to the metatheory
 
 This module contains functions that are meant to be called from Haskell code.
@@ -336,4 +340,4 @@ alphaU plc1 plc2 | inj₂ plc1' | inj₂ plc2' | _ | _ = Bool.false
 alphaU plc1 plc2 | _ | _ = Bool.false
  
 {-# COMPILE GHC alphaU as alphaU #-}
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Main.lagda.md b/plutus-metatheory/src/Main.lagda.md
index 92350cceb1b..3f50c43491a 100644
--- a/plutus-metatheory/src/Main.lagda.md
+++ b/plutus-metatheory/src/Main.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Main
+layout: page
+---
 ```
 module Main where
 
diff --git a/plutus-metatheory/src/Raw.lagda.md b/plutus-metatheory/src/Raw.lagda.md
index 743ad028ea0..556999458e1 100644
--- a/plutus-metatheory/src/Raw.lagda.md
+++ b/plutus-metatheory/src/Raw.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Raw
+layout: page
+---
 ```
 module Raw where
 ```
@@ -180,4 +184,4 @@ rawListPrinter [] = ""
 rawListPrinter (x ∷ []) = rawPrinter x
 rawListPrinter (x ∷ y ∷ xs) = rawPrinter x ++ " , " ++ rawListPrinter (y ∷ xs)                               
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/RawU.lagda.md b/plutus-metatheory/src/RawU.lagda.md
index 706457c26b9..b5f0af9fa98 100644
--- a/plutus-metatheory/src/RawU.lagda.md
+++ b/plutus-metatheory/src/RawU.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Raw - Interface to Haskell
+layout: page
+---
 
 This module provides the interface between the Haskell code and the Agda code.
 It replicates the Haskell representation of Raw. In particular, for term constants,
diff --git a/plutus-metatheory/src/Scoped.lagda.md b/plutus-metatheory/src/Scoped.lagda.md
index 4ea4bf0bb4f..6a8c80c13b7 100644
--- a/plutus-metatheory/src/Scoped.lagda.md
+++ b/plutus-metatheory/src/Scoped.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped
+layout: page
+---
 ```
 module Scoped where
 ```
diff --git a/plutus-metatheory/src/Scoped/Extrication.lagda.md b/plutus-metatheory/src/Scoped/Extrication.lagda.md
index 0250e0963a7..04395a8eb77 100644
--- a/plutus-metatheory/src/Scoped/Extrication.lagda.md
+++ b/plutus-metatheory/src/Scoped/Extrication.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication
+layout: page
+---
 ```
 module Scoped.Extrication where
 ```
diff --git a/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
index 5731dabe73b..67497acaa9a 100644
--- a/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Scoped/Extrication/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.Extrication.RenamingSubstitution
+layout: page
+---
 ```
 module Scoped.Extrication.RenamingSubstitution where
 ```
diff --git a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
index 141afe7e917..8ec242565d6 100644
--- a/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Scoped/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Scoped.RenamingSubstitution
+layout: page
+---
 ```
 module Scoped.RenamingSubstitution where
 ```
diff --git a/plutus-metatheory/src/Type/BetaNBE.lagda.md b/plutus-metatheory/src/Type/BetaNBE.lagda.md
index 8e896de1d2f..75288d17d32 100644
--- a/plutus-metatheory/src/Type/BetaNBE.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE
+layout: page
+---
 ```
 module Type.BetaNBE where
 ```
@@ -187,4 +191,4 @@ module _ where
               → lookup (eval-VecList Tss η) e ≡ eval-List (lookup Tss e) η
   lookup-eval-VecList zero (_ ∷ _) η = refl
   lookup-eval-VecList (suc e) (_ ∷ Tss) η = lookup-eval-VecList e Tss η
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
index f289c166b74..d740d8102f6 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Completeness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Completeness
+layout: page
+---
 ```
 module Type.BetaNBE.Completeness where
 ```
diff --git a/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md b/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
index 8771f68d1b5..4dd3863bcc2 100644
--- a/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/RenamingSubstitution.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.RenamingSubstitution
+layout: page
+---
 ```
 module Type.BetaNBE.RenamingSubstitution where
 
diff --git a/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
index d03c9feafdd..dc5c6e364e2 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Soundness.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Soundness
+layout: page
+---
 ```
 module Type.BetaNBE.Soundness where
 ```
diff --git a/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md b/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
index 327490aa7b6..f07bc23d42b 100644
--- a/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNBE/Stability.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNBE.Stability
+layout: page
+---
 ```
 module Type.BetaNBE.Stability where
 ```
diff --git a/plutus-metatheory/src/Type/BetaNormal.lagda.md b/plutus-metatheory/src/Type/BetaNormal.lagda.md
index 6e64fb85bdf..bcbc7771fd4 100644
--- a/plutus-metatheory/src/Type/BetaNormal.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNormal.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNormal
+layout: page
+---
 ```
 module Type.BetaNormal where
 ```
diff --git a/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md b/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
index 2adcfa29454..4ffcd817ee2 100644
--- a/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
+++ b/plutus-metatheory/src/Type/BetaNormal/Equality.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Type.BetaNormal.Equality
+layout: page
+---
 ```
 module Type.BetaNormal.Equality where
 ```
@@ -134,4 +138,4 @@ renNf-comp-VecList [] = refl
 renNf-comp-VecList (xs ∷ xss) = cong₂ _∷_ (renNf-comp-List xs) (renNf-comp-VecList xss)
 
 ```
- 
\ No newline at end of file
+ 
diff --git a/plutus-metatheory/src/Untyped/CEK.lagda.md b/plutus-metatheory/src/Untyped/CEK.lagda.md
index 6a0ebfe4c79..f3915779ca4 100644
--- a/plutus-metatheory/src/Untyped/CEK.lagda.md
+++ b/plutus-metatheory/src/Untyped/CEK.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Untyped.CEK
+layout: page
+---
 ```
 {-# OPTIONS --type-in-type #-}
 
diff --git a/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md b/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
index dff944ff137..635fba0b62d 100644
--- a/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
+++ b/plutus-metatheory/src/Untyped/CEKWithCost.lagda.md
@@ -1,3 +1,7 @@
+---
+title: CEK Machine with Costs
+layout: page
+---
 # CEK Machine with costs
 
 This module implements a CEK machine for UPLC which computes costs.
@@ -227,4 +231,4 @@ cekStepperEquivalence (suc n) s rewrite sym (cekStepEquivalence s) with step s
 ... | s ◅ v = cekStepperEquivalence n  (s ◅ v)
 ... | □ x = refl
 ... | ◆ = refl
-``` 
\ No newline at end of file
+``` 
diff --git a/plutus-metatheory/src/Utils.lagda.md b/plutus-metatheory/src/Utils.lagda.md
index cbeba0e86ce..94216fbff09 100644
--- a/plutus-metatheory/src/Utils.lagda.md
+++ b/plutus-metatheory/src/Utils.lagda.md
@@ -1,3 +1,7 @@
+---
+title: Utils
+layout: page
+---
 ```
 module Utils where
 ```
diff --git a/plutus-metatheory/src/Utils/Decidable.lagda.md b/plutus-metatheory/src/Utils/Decidable.lagda.md
index 5723eafaa32..3da35c2920a 100644
--- a/plutus-metatheory/src/Utils/Decidable.lagda.md
+++ b/plutus-metatheory/src/Utils/Decidable.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.Decidable
+layout: page
+---
 ```
 module Utils.Decidable where
 ```
@@ -54,4 +57,4 @@ dhcong₂ : ∀ {α β γ} {A : Set α} {B B' : A → Set β} {C : Set γ} {x₁
         → Dec (f x₁ y₁ z₁ ≡ f x₂ y₂ z₂)
 dhcong₂ f inj (yes refl) qy qz = dcong₂ (f _) ((λ { (refl ,, yy) → yy }) ∘ inj) (qy _) (qz _)
 dhcong₂ f inj (no  c)    _  _  = no λ {p → c (proj₁ (inj p))}
-```
\ No newline at end of file
+```
diff --git a/plutus-metatheory/src/Utils/List.lagda.md b/plutus-metatheory/src/Utils/List.lagda.md
index bee5c93b3a3..e4ea65f6bc0 100644
--- a/plutus-metatheory/src/Utils/List.lagda.md
+++ b/plutus-metatheory/src/Utils/List.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.List
+layout: page
+---
 ```
 module Utils.List where
 ```
@@ -509,4 +512,4 @@ equalbyPredicateI {bs = bs}{bs'}{fs}{fs'}{tot} TOT {Bs} {Bs'} {Fs} {Fs'} {h} {h'
 ... | pbs , snd with <>>[]-cancelʳ bs bs' pbs 
 equalbyPredicateI TOT {Bs} {Bs'} P p p' q q' ps ps' ¬PH ¬PH' 
      | refl , refl , refl , pBs | refl with <>>I[]-cancelʳ Bs Bs' pBs 
-... | refl = refl , refl , refl , refl
\ No newline at end of file
+... | refl = refl , refl , refl , refl
diff --git a/plutus-metatheory/src/Utils/Reflection.lagda.md b/plutus-metatheory/src/Utils/Reflection.lagda.md
index 8406a97a6be..7547d6b78bf 100644
--- a/plutus-metatheory/src/Utils/Reflection.lagda.md
+++ b/plutus-metatheory/src/Utils/Reflection.lagda.md
@@ -1,4 +1,7 @@
-
+---
+title: Utils.Reflection
+layout: page
+---
 
 ```
 module Utils.Reflection where
@@ -118,4 +121,4 @@ defListConstructors T defName = do
        d ← getDefinition T
        let cls = clause [] [] (mkList (map (λ q → con q []) (constructors d)))
        defineFun defName (cls ∷ [])
-```
\ No newline at end of file
+```