diff --git a/Bookshelf/Combinator/Aviary.lean b/Bookshelf/Combinator/Aviary.lean
index 2288e59..966ca98 100644
--- a/Bookshelf/Combinator/Aviary.lean
+++ b/Bookshelf/Combinator/Aviary.lean
@@ -13,8 +13,7 @@ use. Their inclusion here serves more as pseudo-documentation than anything.
university press, 2000.
-/
-/--
-#### Bald Eagle
+/-- #### Bald Eagle
`E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)`
-/
@@ -22,36 +21,31 @@ def E' (x : α → β → γ)
(y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε)
(z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃)
-/--
-#### Becard
+/-- #### Becard
`B₃xyzw = x(y(zw))`
-/
def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w))
-/--
-#### Blackbird
+/-- #### Blackbird
`B₁xyzw = x(yzw)`
-/
def B₁ (x : α → ε) (y : β → γ → α) (z : β) (w : γ) := x (y z w)
-/--
-#### Bluebird
+/-- #### Bluebird
`Bxyz = x(yz)`
-/
def B (x : α → γ) (y : β → α) (z : β) := x (y z)
-/--
-#### Bunting
+/-- #### Bunting
`B₂xyzwv = x(yzwv)`
-/
def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v)
-/--
-#### Cardinal Once Removed
+/-- #### Cardinal Once Removed
`C*xyzw = xywz`
-/
@@ -59,50 +53,48 @@ def C_star (x : α → β → γ → δ) (y : α) (z : γ) (w : β) := x y w z
notation "C*" => C_star
-/--
-#### Cardinal
+/-- #### Cardinal
`Cxyz = xzy`
-/
def C (x : α → β → δ) (y : β) (z : α) := x z y
-/--
-#### Converse Warbler
+/-- #### Converse Warbler
`W'xy = yxx`
-/
def W' (x : α) (y : α → α → β) := y x x
-/--
-#### Dickcissel
+/-- #### Dickcissel
`D₁xyzwv = xyz(wv)`
-/
def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v)
-/--
-#### Dove
+/-! #### Double Mockingbird
+
+`M₂xy = xy(xy)`
+-/
+
+/-- #### Dove
`Dxyzw = xy(zw)`
-/
def D (x : α → γ → δ) (y : α) (z : β → γ) (w : β) := x y (z w)
-/--
-#### Dovekie
+/-- #### Dovekie
`D₂xyzwv = x(yz)(wv)`
-/
def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v)
-/--
-#### Eagle
+/-- #### Eagle
`Exyzwv = xy(zwv)`
-/
def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v)
-/--
-#### Finch Once Removed
+/-- #### Finch Once Removed
`F*xyzw = xwzy`
-/
@@ -110,99 +102,95 @@ def F_star (x : α → β → γ → δ) (y : γ) (z : β) (w : α) := x w z y
notation "F*" => F_star
-/--
-#### Finch
+/-- #### Finch
`Fxyz = zyx`
-/
def F (x : α) (y : β) (z : β → α → γ) := z y x
-/--
-#### Goldfinch
+/-- #### Goldfinch
`Gxyzw = xw(yz)`
-/
def G (x : α → γ → δ) (y : β → γ) (z : β) (w : α) := x w (y z)
-/--
-#### Hummingbird
+/-- #### Hummingbird
`Hxyz = xyzy`
-/
def H (x : α → β → α → γ) (y : α) (z : β) := x y z y
-/--
-#### Identity Bird
+/-- #### Identity Bird
`Ix = x`
-/
def I (x : α) : α := x
-/--
-#### Kestrel
+/-- #### Kestrel
`Kxy = x`
-/
def K (x : α) (_ : β) := x
-/--
-#### Owl
+/-! #### Lark
+
+`Lxy = x(yy)`
+-/
+
+/-! #### Mockingbird
+
+`Mx = xx`
+-/
+
+/-- #### Owl
`Oxy = y(xy)`
-/
def O (x : (α → β) → α) (y : α → β) := y (x y)
-/--
-#### Phoenix
+/-- #### Phoenix
`Φxyzw = x(yw)(zw)`
-/
def Φ (x : β → γ → δ) (y : α → β) (z : α → γ) (w : α) := x (y w) (z w)
-/--
-#### Psi Bird
+/-- #### Psi Bird
`Ψxyzw = x(yz)(yw)`
-/
def Ψ (x : α → α → γ) (y : β → α) (z : β) (w : β) := x (y z) (y w)
-/--
-#### Quacky Bird
+/-- #### Quacky Bird
`Q₄xyz = z(yx)`
-/
def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x)
-/--
-#### Queer Bird
+/-- #### Queer Bird
`Qxyz = y(xz)`
-/
def Q (x : α → β) (y : β → γ) (z : α) := y (x z)
-/--
-#### Quirky Bird
+/-- #### Quirky Bird
`Q₃xyz = z(xy)`
-/
def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y)
-/--
-#### Quixotic Bird
+/-- #### Quixotic Bird
`Q₁xyz = x(zy)`
-/
def Q₁ (x : α → γ) (y : β) (z : β → α) := x (z y)
-/--
-#### Quizzical Bird
+/-- #### Quizzical Bird
`Q₂xyz = y(zx)`
-/
def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x)
-/--
-#### Robin Once Removed
+/-- #### Robin Once Removed
`R*xyzw = xzwy`
-/
@@ -210,36 +198,36 @@ def R_star (x : α → β → γ → δ) (y : γ) (z : α) (w : β) := x z w y
notation "R*" => R_star
-/--
-#### Robin
+/-- #### Robin
`Rxyz = yzx`
-/
def R (x : α) (y : β → α → γ) (z : β) := y z x
-/--
-#### Sage Bird
+/-- #### Sage Bird
`Θx = x(Θx)`
-/
partial def Θ [Inhabited α] (x : α → α) := x (Θ x)
-/--
-#### Starling
+/-- #### Starling
`Sxyz = xz(yz)`
-/
def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
-/--
-#### Thrush
+/-- #### Thrush
`Txy = yx`
-/
def T (x : α) (y : α → β) := y x
-/--
-#### Vireo Once Removed
+/-! #### Turing Bird
+
+`Uxy = y(xxy)`
+-/
+
+/-- #### Vireo Once Removed
`V*xyzw = xwyz`
-/
@@ -247,15 +235,13 @@ def V_star (x : α → β → γ → δ) (y : β) (z : γ) (w : α) := x w y z
notation "V*" => V_star
-/--
-#### Vireo
+/-- #### Vireo
`Vxyz = zxy`
-/
def V (x : α) (y : β) (z : α → β → γ) := z x y
-/--
-#### Warbler
+/-- #### Warbler
`Wxy = xyy`
-/
diff --git a/Bookshelf/Combinator/Aviary_html.html b/Bookshelf/Combinator/Aviary_html.html
deleted file mode 100644
index 4dbad5d..0000000
--- a/Bookshelf/Combinator/Aviary_html.html
+++ /dev/null
@@ -1,58 +0,0 @@
-
-
-
-
-
- Bookshelf.Combinator.Aviary
-
-
-
-
- Bookshelf.Combinator.Aviary
-
- A list of birds as defined in To Mock a Mockingbird.
- Refer to Bookshelf/Combinator/Aviary
- for implementation examples.
-
-
- - Bald Eagle: \(\hat{E}xy_1y_2y_3z_1z_2z_3 = x(y_1y_2y_3)(z_1z_2z_3)\)
- - Becard: \(B_3xyzw = x(y(zw))\)
- - Blackbird: \(B_1xyzw = x(yzw)\)
- - Bluebird: \(Bxyz = x(yz)\)
- - Bunting: \(B_2xyzwv = x(yzwv)\)
- - Cardinal Once Removed: \(C^*xyzw = xywz\)
- - Cardinal: \(Cxyz = xzy\)
- - Converse Warbler: \(W'xy = yxx\)
- - Dickcissel: \(D_1xyzwv = xyz(wv)\)
- - Double Mockingbird: \(M_2xy = xy(xy)\)
- - Dove: \(Dxyzw = xy(zw)\)
- - Dovekie: \(D_2xyzwv = x(yz)(wv)\)
- - Eagle: \(Exyzwv = xy(zwv)\)
- - Finch Once Removed: \(F^*xyzw = xwzy\)
- - Finch: \(Fxyz = zyx\)
- - Goldfinch: \(Gxyzw = xw(yz)\)
- - Hummingbird: \(Hxyz = xyzy\)
- - Identity Bird: \(Ix = x\)
- - Kestrel: \(Kxy = x\)
- - Lark: \(Lxy = x(yy)\)
- - Mockingbird: \(Mx = xx\)
- - Owl: \(Oxy = y(xy)\)
- - Phoenix: \(\Phi xyzw = x(yw)(zw)\)
- - Psi Bird: \(\Psi xyzw = x(yz)(yw)\)
- - Quacky Bird: \(Q_4xyz = z(yx)\)
- - Queer Bird: \(Qxyz = y(xz)\)
- - Quirky Bird: \(Q_3xyz = z(xy)\)
- - Quixotic Bird: \(Q_1xyz = x(zy)\)
- - Quizzical Bird: \(Q_2xyz = y(zx)\)
- - Robin Once Removed: \(R^*xyzw = xzwy\)
- - Robin: \(Rxyz = yzx\)
- - Sage Bird: \(\Theta x = x(\Theta x)\)
- - Starling: \(Sxyz = xz(yz)\)
- - Thrush: \(Txy = yx\)
- - Turing Bird: \(Uxy = y(xxy)\)
- - Vireo Once Removed: \(V^*xyzw = xwyz\)
- - Vireo: \(Vxyz = zxy\)
- - Warbler: \(Wxy = xyy\)
-
-
-