Initial commit

Author: splintersuidman

.gitignore

@@ -0,0 +1,5 @@
+# Agda
+*.agdai
+
+# Emacs
+\#*#

CombinatoryLogic/Equality.agda

@@ -0,0 +1,139 @@
+-- Kapitel 1, Abschnitt D (Die Eigenschaften der Gleichheit)
+module CombinatoryLogic.Equality where
+
+open import Algebra.Definitions using (Congruent₂; LeftCongruent; RightCongruent)
+open import Data.Vec using (Vec; []; _∷_; foldr₁; lookup)
+open import Function using (_$_)
+open import Relation.Binary using (IsEquivalence; Setoid)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open import CombinatoryLogic.Semantics
+open import CombinatoryLogic.Syntax
+
+private
+  -- A lemma used in the proofs of Propositions 1 and 2.
+  lemma-CQXX : ∀ {X} → ⊢ C ∙ Q ∙ X ∙ X
+  lemma-CQXX {X} =
+    let s₁ = ⊢ Π ∙ (W ∙ (C ∙ Q))                        [ ax Q ]
+        s₂ = ⊢ W ∙ (C ∙ Q) ∙ X                          [ Π s₁ ]
+        s₃ = ⊢ Q ∙ (W ∙ (C ∙ Q) ∙ X) ∙ (C ∙ Q ∙ X ∙ X)  [ W ]
+        s₄ = ⊢ C ∙ Q ∙ X ∙ X                            [ Q₁ s₂ s₃ ]
+    in s₄
+
+-- Satz 1
+prop₁ : ∀ {X} → ⊢ Q ∙ X ∙ X
+prop₁ {X} = s₆ where
+  s₄ = ⊢ C ∙ Q ∙ X ∙ X                            [ lemma-CQXX ]
+  s₅ = ⊢ Q ∙ (C ∙ Q ∙ X ∙ X) ∙ (Q ∙ X ∙ X)        [ C ]
+  s₆ = ⊢ Q ∙ X ∙ X                                [ Q₁ s₄ s₅ ]
+
+-- Satz 2
+prop₂ : ∀ {X Y} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ Y ∙ X
+prop₂ {X} {Y} ⊢QXY = s₅ where
+  s₁ = ⊢ Q ∙ X ∙ Y                             [ ⊢QXY ]
+  -- NOTE: Curry's proof contains a mistake: CQXX should be CQXY.
+  s₂ = ⊢ Q ∙ (C ∙ Q ∙ X ∙ X) ∙ (C ∙ Q ∙ X ∙ Y) [ Q₂ {Z = C ∙ Q ∙ X} s₁ ]
+  s₃ = ⊢ C ∙ Q ∙ X ∙ X                         [ lemma-CQXX ]
+  -- NOTE: Curry's proof uses rule Q, but there is no such rule.
+  s₄ = ⊢ C ∙ Q ∙ X ∙ Y                         [ Q₁ s₃ s₂ ]
+  s₅ = ⊢ Q ∙ Y ∙ X                             [ Q₁ s₄ C ]
+
+-- Satz 3
+prop₃ : ∀ {X Y Z} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ Y ∙ Z → ⊢ Q ∙ X ∙ Z
+prop₃ {X} {Y} {Z} ⊢QXY ⊢QYZ = s₃ where
+  s₁ = ⊢ Q ∙ Y ∙ Z                     [ ⊢QYZ ]
+  s₂ = ⊢ Q ∙ (Q ∙ X ∙ Y) ∙ (Q ∙ X ∙ Z) [ Q₂ {Z = Q ∙ X} s₁ ]
+  s₃ = ⊢ Q ∙ X ∙ Z                     [ Q₁ ⊢QXY s₂ ]
+
+-- Satz 4
+prop₄ : ∀ {X Y Z} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ (X ∙ Z) ∙ (Y ∙ Z)
+prop₄ {X} {Y} {Z} Hp = s₅ where
+  p₁ = λ {X} → ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (B ∙ (W ∙ K) ∙ X ∙ Z)  [ C ]
+  p₂ = λ {X} → ⊢ Q ∙ (B ∙ (W ∙ K) ∙ X ∙ Z) ∙ (W ∙ K ∙ (X ∙ Z))            [ B ]
+  p₃ = λ {X} → ⊢ Q ∙ (W ∙ K ∙ (X ∙ Z)) ∙ (K ∙ (X ∙ Z) ∙ (X ∙ Z))          [ W ]
+  p₄ = λ {X} → ⊢ Q ∙ (K ∙ (X ∙ Z) ∙ (X ∙ Z)) ∙ (X ∙ Z)                    [ K ]
+  p₅ = λ {X} → ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (X ∙ Z)                [ prop₃ p₁ $ prop₃ p₂ $ prop₃ p₃ p₄ ]
+  s₁ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ Y)  [ Q₂ Hp ]
+  s₂ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (X ∙ Z)                      [ p₅ ]
+  s₃ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ Y) ∙ (Y ∙ Z)                      [ p₅ ]
+  s₄ = ⊢ Q ∙ (X ∙ Z) ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X)                      [ prop₂ s₂ ]
+  s₅ = ⊢ Q ∙ (X ∙ Z) ∙ (Y ∙ Z)                                          [ prop₃ s₄ $ prop₃ s₁ s₃ ]
+
+-- Satz 5
+prop₅ : ∀ {X Y} → X ≡ Y → ⊢ Q ∙ X ∙ Y
+prop₅ {X} {Y} refl = prop₁
+
+-- Satz 6 (first part)
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record
+  { refl = prop₁
+  ; sym = prop₂
+  ; trans = prop₃
+  }
+
+setoid : Setoid _ _
+setoid = record
+  { Carrier = Combinator
+  ; _≈_ = _≈_
+  ; isEquivalence = isEquivalence
+  }
+
+module Reasoning where
+  module ≈ = IsEquivalence isEquivalence
+  import Relation.Binary.Reasoning.Base.Single _≈_ ≈.refl ≈.trans as Base
+  open Base using (begin_; _∎) public
+
+  infixr 2 _≈⟨⟩_ step-≈ step-≈˘
+
+  _≈⟨⟩_ : ∀ x {y} → x Base.IsRelatedTo y → x Base.IsRelatedTo y
+  _ ≈⟨⟩ x≈y = x≈y
+
+  step-≈ = Base.step-∼
+  syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z
+
+  step-≈˘ : ∀ x {y z} → y Base.IsRelatedTo z → y ≈ x → x Base.IsRelatedTo z
+  step-≈˘ x y∼z y≈x = x ≈⟨ ≈.sym y≈x ⟩ y∼z
+  syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z
+
+-- Satz 6 (second part)
+∙-cong : Congruent₂ _≈_ _∙_
+∙-cong {X} {X′} {Y} {Y′} ⊢X==X′ ⊢Y==Y′ = s₃ where
+  s₁ = ⊢ X ∙ Y == X ∙ Y′    [ Q₂ ⊢Y==Y′ ]
+  s₂ = ⊢ X ∙ Y′ == X′ ∙ Y′  [ prop₄ ⊢X==X′ ]
+  s₃ = ⊢ X ∙ Y == X′ ∙ Y′   [ prop₃ s₁ s₂ ]
+
+-- ∙-congˡ and ∙-congʳ follow from ∙-cong, but are also just different names for
+-- Q₂ and prop₄, respectively.
+∙-congˡ : LeftCongruent _≈_ _∙_
+∙-congˡ = Q₂
+
+∙-congʳ : RightCongruent _≈_ _∙_
+∙-congʳ = prop₄
+
+-- TODO: Satz 7, 8
+
+prop₉ : ∀ {X} → ⊢ I ∙ X == X
+prop₉ {X} = begin
+  I ∙ X      ≈⟨⟩
+  W ∙ K ∙ X  ≈⟨ W ⟩
+  K ∙ X ∙ X  ≈⟨ K ⟩
+  X          ∎
+  where open Reasoning
+
+-- Note after the proof of Satz 9.
+S : Combinator
+S = B ∙ (B ∙ W) ∙ (B ∙ B ∙ C)
+
+prop-S : ∀ {X} {Y} {Z} → ⊢ S ∙ X ∙ Y ∙ Z == X ∙ Z ∙ (Y ∙ Z)
+prop-S {X} {Y} {Z} = begin
+  S ∙ X ∙ Y ∙ Z ≈⟨⟩
+  B ∙ (B ∙ W) ∙ (B ∙ B ∙ C) ∙ X ∙ Y ∙ Z  ≈⟨ ∙-congʳ $ ∙-congʳ B ⟩
+  B ∙ W ∙ (B ∙ B ∙ C ∙ X) ∙ Y ∙ Z        ≈⟨ ∙-congʳ B ⟩
+  W ∙ (B ∙ B ∙ C ∙ X ∙ Y) ∙ Z            ≈⟨ W ⟩
+  B ∙ B ∙ C ∙ X ∙ Y ∙ Z ∙ Z              ≈⟨ ∙-congʳ $ ∙-congʳ $ ∙-congʳ B ⟩
+  B ∙ (C ∙ X) ∙ Y ∙ Z ∙ Z                ≈⟨ ∙-congʳ B ⟩
+  C ∙ X ∙ (Y ∙ Z) ∙ Z                    ≈⟨ C ⟩
+  X ∙ Z ∙ (Y ∙ Z)                        ∎
+  where open Reasoning
+
+-- TODO: ⊢ B == S(KS)K, ⊢ C == S(BBS)(KK), ⊢ W == SS(SK), ⊢ I == SKK

CombinatoryLogic/Forest.agda

@@ -0,0 +1,61 @@
+module CombinatoryLogic.Forest where
+
+open import Data.Product using (_,_)
+open import Function using (_$_)
+open import Mockingbird.Forest using (Forest)
+
+open import CombinatoryLogic.Equality as Equality using (isEquivalence; ∙-cong)
+open import CombinatoryLogic.Semantics as ⊢ using (_≈_)
+open import CombinatoryLogic.Syntax as Syntax using (Combinator)
+
+forest : Forest
+forest = record
+  { Bird = Combinator
+  ; _≈_ = _≈_
+  ; _∙_ = Syntax._∙_
+  ; isForest = record
+    { isEquivalence = isEquivalence
+    ; ∙-cong = ∙-cong
+    }
+  }
+
+open Forest forest
+
+open import Mockingbird.Forest.Birds forest
+open import Mockingbird.Forest.Extensionality forest
+import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
+import Mockingbird.Problems.Chapter12 forest as Chapter₁₂
+
+instance
+  hasWarbler : HasWarbler
+  hasWarbler = record
+    { W = Syntax.W
+    ; isWarbler = λ _ _ → ⊢.W
+    }
+
+  hasKestrel : HasKestrel
+  hasKestrel = record
+    { K = Syntax.K
+    ; isKestrel = λ _ _ → ⊢.K
+    }
+
+  hasBluebird : HasBluebird
+  hasBluebird = record
+    { B = Syntax.B
+    ; isBluebird = λ _ _ _ → ⊢.B
+    }
+
+  hasIdentity : HasIdentity
+  hasIdentity = record
+    { I = Syntax.I
+    ; isIdentity = λ _ → Equality.prop₉
+    }
+
+  hasMockingbird : HasMockingbird
+  hasMockingbird = Chapter₁₁.problem₁₄
+
+  hasLark : HasLark
+  hasLark = Chapter₁₂.problem₃
+
+  hasComposition : HasComposition
+  hasComposition = Chapter₁₁.problem₁

CombinatoryLogic/Semantics.agda

@@ -0,0 +1,62 @@
+module CombinatoryLogic.Semantics where
+
+open import Relation.Binary using (Rel)
+
+open import CombinatoryLogic.Syntax
+
+-- Kapitel 1, Abschnitt C, §5 (Axiome)
+data Axiom : Combinator → Set where
+  Q : Axiom (Π ∙ (W ∙ (C ∙ Q)))
+  B : Axiom (C ∙ (B ∙ B ∙ (B ∙ B ∙ B)) ∙ B == B ∙ (B ∙ B) ∙ B)
+  C : Axiom (C ∙ (B ∙ B ∙ (B ∙ B ∙ B)) ∙ W ∙ C == B ∙ (B ∙ C) ∙ (B ∙ B ∙ B))
+  W : Axiom (C ∙ (B ∙ B ∙ B) ∙ W == B ∙ (B ∙ W) ∙ (B ∙ B ∙ B))
+  -- NOTE (Curry): this axiom can be proved from the others.
+  I₁ : Axiom (C ∙ (B ∙ B ∙ B) ∙ K == B ∙ (B ∙ K) ∙ I)
+  BC : Axiom (B ∙ B ∙ C == B ∙ (B ∙ (B ∙ C) ∙ C) ∙ (B ∙ B))
+  BW : Axiom (B ∙ B ∙ W == B ∙ (B ∙ (B ∙ (B ∙ (B ∙ W) ∙ W) ∙ (B ∙ C)) ∙ B ∙ (B ∙ B)) ∙ B)
+  BK : Axiom (B ∙ B ∙ K == B ∙ K ∙ K)
+  CC₁ : Axiom (B ∙ C ∙ C ∙ B ∙ (B ∙ I))
+  CC₂ : Axiom (B ∙ (B ∙ (B ∙ C) ∙ C) ∙ (B ∙ C) == B ∙ (B ∙ C ∙ (B ∙ C)) ∙ C)
+  CW : Axiom (B ∙ C ∙ W == B ∙ (B ∙ (B ∙ W) ∙ C) ∙ (B ∙ C))
+  CK : Axiom (B ∙ C ∙ K == B ∙ K)
+  WC : Axiom (B ∙ W ∙ C == W)
+  WW : Axiom (B ∙ W ∙ W == B ∙ W ∙ (B ∙ W))
+  WK : Axiom (B ∙ W ∙ K == B ∙ I)
+  I₂ : Axiom (B ∙ I == I)
+
+-- TODO: fixity definition
+infix 4 ⊢_
+
+-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Festsetzung 1
+data ⊢_ : Combinator → Set where
+  ax : ∀ {X} → Axiom X → ⊢ X
+
+  -- Kapitel 1, Abschnitt C, §6 (Regeln)
+  Q₁ : ∀ {X Y} → ⊢ X → ⊢ X == Y → ⊢ Y
+  Q₂ : ∀ {X Y Z} → ⊢ X == Y → ⊢ Z ∙ X == Z ∙ Y
+  Π : ∀ {X Y} → ⊢ Π ∙ X → ⊢ X ∙ Y
+  B : ∀ {X Y Z} → ⊢ B ∙ X ∙ Y ∙ Z == X ∙ (Y ∙ Z)
+  C : ∀ {X Y Z} → ⊢ C ∙ X ∙ Y ∙ Z == X ∙ Z ∙ Y
+  W : ∀ {X Y} → ⊢ W ∙ X ∙ Y == X ∙ Y ∙ Y
+  K : ∀ {X Y} → ⊢ K ∙ X ∙ Y == X
+  P : ∀ {X Y} → ⊢ X → ⊢ P ∙ X ∙ Y → ⊢ Y
+  ∧ : ∀ {X Y} → ⊢ X → ⊢ Y → ⊢ ∧ ∙ X ∙ Y
+
+-- We introduce convenience notation for the equality defined in Kapitel 1,
+-- Abschnitt C, §4 (Symbolische Festsetzungen), Festsetzung 3 (Gleichheit).
+_≈_ : Rel Combinator _
+X ≈ Y = ⊢ X == Y
+
+infix 0 _[_]
+
+-- An operator that helps write proofs in the style of Curry. Where Curry writes
+--   ⟨statement⟩ (⟨rule⟩)
+-- we write
+--   ⟨statement⟩ [ ⟨rule⟩ ]
+--
+-- Later, we can also use the Agda standard library's reasoning combinators
+-- (e.g. _≈⟨_⟩_) for proving equalities, but not before it is shown that the
+-- equality _≈_ is an equivalence relation, which Curry does in propositions 1,
+-- 2 and 3 of Kapitel 1, Abschnitt D (Die Eigenschaften der Gleichheit).
+_[_] : ∀ {a} (A : Set a) (x : A) → A
+_ [ x ] = x

CombinatoryLogic/Syntax.agda

@@ -0,0 +1,51 @@
+module CombinatoryLogic.Syntax where
+
+open import Data.String using (String; _++_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 1
+infixl 6 _∙_
+
+data Combinator : Set where
+  -- Kapitel 1, Abschnitt C, §3 (Die formalen Grundbegriffe)
+  B C W K Q Π P ∧ : Combinator
+  -- Kapitel 1, Abschnitt C, §2, c (Anwendung)
+  _∙_ : (X Y : Combinator) → Combinator
+
+-- NOTE: for the (intensional) equality defined by Kapitel 1, Abschnitt C, §4
+-- (Symbolische Festsetzungen), Festsetzung 2, we use the propositional equality
+-- _≡_.
+
+toString : Combinator → String
+toString (X ∙ Y@(_ ∙ _)) = toString X ++ "(" ++ toString Y ++ ")"
+toString (X ∙ Y) = toString X ++ toString Y
+toString B = "B"
+toString C = "C"
+toString W = "W"
+toString K = "K"
+toString Q = "Q"
+toString Π = "Π"
+toString P = "P"
+toString ∧ = "∧"
+
+_ : toString (K ∙ Q ∙ (W ∙ C)) ≡ "KQ(WC)"
+_ = refl
+
+_ : toString (K ∙ ∧ ∙ (Q ∙ Π) ∙ (W ∙ C)) ≡ "K∧(QΠ)(WC)"
+_ = refl
+
+_ : toString (K ∙ ∧ ∙ ((Q ∙ Π) ∙ (W ∙ C))) ≡ "K∧(QΠ(WC))"
+_ = refl
+
+_ : toString (K ∙ K ∙ K) ≡ "KKK"
+_ = refl
+
+infix 5 _==_
+
+-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 2
+_==_ : (X Y : Combinator) → Combinator
+X == Y = Q ∙ X ∙ Y
+
+-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 3
+I : Combinator
+I = W ∙ K

LICENCE

@@ -0,0 +1,7 @@
+Copyright © 2021 Splinter Suidman
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Mockingbird/Forest.agda

@@ -0,0 +1,3 @@
+module Mockingbird.Forest where
+
+open import Mockingbird.Forest.Base public

Mockingbird/Forest/Base.agda

@@ -0,0 +1,52 @@
+module Mockingbird.Forest.Base where
+
+open import Algebra using (Op₂; Congruent₂; LeftCongruent; RightCongruent)
+open import Level using (_⊔_) renaming (suc to lsuc)
+open import Relation.Binary using (Rel; IsEquivalence; Setoid)
+open import Relation.Nullary using (¬_)
+
+record IsForest {b ℓ} (Bird : Set b) (_≈_ : Rel Bird ℓ) (_∙_ : Op₂ Bird) : Set (b ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    ∙-cong : Congruent₂ _≈_ _∙_
+
+  open IsEquivalence isEquivalence public
+
+  setoid : Setoid b ℓ
+  setoid = record { isEquivalence = isEquivalence }
+
+  ∙-congˡ : LeftCongruent _≈_ _∙_
+  ∙-congˡ A≈B = ∙-cong refl A≈B
+
+  ∙-congʳ : RightCongruent _≈_ _∙_
+  ∙-congʳ A≈B = ∙-cong A≈B refl
+
+record Forest {b ℓ} : Set (lsuc (b ⊔ ℓ)) where
+  infix  4 _≈_
+  infixl 6 _∙_
+
+  field
+    Bird : Set b
+    _≈_ : Rel Bird ℓ
+    _∙_ : Op₂ Bird
+    isForest : IsForest Bird _≈_ _∙_
+
+  _≉_ : Rel Bird ℓ
+  x ≉ y = ¬ (x ≈ y)
+
+  open IsForest isForest public
+
+  import Relation.Binary.Reasoning.Base.Single _≈_ refl trans as Base
+  open Base using (begin_; _∎) public
+
+  infixr 2 _≈⟨⟩_ step-≈ step-≈˘
+
+  _≈⟨⟩_ : ∀ x {y} → x Base.IsRelatedTo y → x Base.IsRelatedTo y
+  _ ≈⟨⟩ x≈y = x≈y
+
+  step-≈ = Base.step-∼
+  syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z
+
+  step-≈˘ : ∀ x {y z} → y Base.IsRelatedTo z → y ≈ x → x Base.IsRelatedTo z
+  step-≈˘ x y∼z y≈x = x ≈⟨ sym y≈x ⟩ y∼z
+  syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z

Mockingbird/Forest/Birds.agda

@@ -0,0 +1,5 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Mockingbird.Forest.Combination.Base public

Mockingbird/Forest/Combination.agda

@@ -0,0 +1,29 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination.Base {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Level using (Level; _⊔_)
+open import Relation.Unary using (Pred; _∈_)
+
+open Forest forest
+
+private
+  variable
+    p : Level
+    x y z : Bird
+    P : Pred Bird p
+
+-- If P is a set of birds, we can think of ⟨ P ⟩ as the set of birds ‘generated
+-- by’ P.
+data ⟨_⟩ (P : Pred Bird p) : Bird → Set (p ⊔ b ⊔ ℓ) where
+  [_] : (x∈P : x ∈ P) → x ∈ ⟨ P ⟩
+
+  _⟨∙⟩_∣_ :
+       (x∈⟨P⟩ : x ∈ ⟨ P ⟩)
+    → (y∈⟨P⟩ : y ∈ ⟨ P ⟩)
+    → (xy≈z : x ∙ y ≈ z)
+    → z ∈ ⟨ P ⟩
+
+infixl 6 _⟨∙⟩_
+_⟨∙⟩_ : x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩ → x ∙ y ∈ ⟨ P ⟩
+_⟨∙⟩_ = _⟨∙⟩_∣ refl

Mockingbird/Forest/Combination/Base.agda

@@ -0,0 +1,45 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination.Properties {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary using (_Respects_)
+open import Relation.Unary using (Pred; _∈_; _⊆_; ∅; _∩_)
+open import Level using (Level; _⊔_)
+
+open Forest forest
+
+open import Mockingbird.Forest.Combination.Base forest
+
+private
+  variable
+    x y z : Bird
+    p : Level
+    P Q : Pred Bird p
+
+subst : P Respects _≈_ → x ≈ y → x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩
+subst respects x≈y [ x∈P ] = [ respects x≈y x∈P ]
+subst respects x≈y (x₁∈⟨P⟩ ⟨∙⟩ x₂∈⟨P⟩ ∣ x₁x₂≈x) = x₁∈⟨P⟩ ⟨∙⟩ x₂∈⟨P⟩ ∣ trans x₁x₂≈x x≈y
+
+subst′ : P Respects _≈_ → y ≈ x → x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩
+subst′ respects y≈x = subst respects (sym y≈x)
+
+-- TODO: maybe lift ∅ to an arbitrary level p
+⟨∅⟩ : ⟨ ∅ ⟩ ⊆ ∅
+⟨∅⟩ (X ⟨∙⟩ Y ∣ xy≈z) = ⟨∅⟩ X
+
+⟨_⟩⊆⟨_⟩ : ∀ {p} (P Q : Pred Bird p) → P ⊆ Q → ⟨ P ⟩ ⊆ ⟨ Q ⟩
+⟨ P ⟩⊆⟨ Q ⟩ P⊆Q [ x∈P ] = [ P⊆Q x∈P ]
+⟨ P ⟩⊆⟨ Q ⟩ P⊆Q (x∈⟨P⟩ ⟨∙⟩ y∈⟨P⟩ ∣ xy≈z) = ⟨ P ⟩⊆⟨ Q ⟩ P⊆Q x∈⟨P⟩ ⟨∙⟩ ⟨ P ⟩⊆⟨ Q ⟩ P⊆Q y∈⟨P⟩ ∣ xy≈z
+
+⟨_∩_⟩ : ∀ {p} (P Q : Pred Bird p) → ⟨ (P ∩ Q) ⟩ ⊆ ⟨ P ⟩ ∩ ⟨ Q ⟩
+⟨ P ∩ Q ⟩ [ (x∈P , x∈Q) ] = ([ x∈P ] , [ x∈Q ])
+⟨ P ∩ Q ⟩ (_⟨∙⟩_∣_ {x} {y} {z} x∈⟨P∩Q⟩ y∈⟨P∩Q⟩ xy≈z) =
+  let (x∈⟨P⟩ , x∈⟨Q⟩) = ⟨_∩_⟩ P Q x∈⟨P∩Q⟩
+      (y∈⟨P⟩ , y∈⟨Q⟩) = ⟨_∩_⟩ P Q y∈⟨P∩Q⟩
+  in (x∈⟨P⟩ ⟨∙⟩ y∈⟨P⟩ ∣ xy≈z , x∈⟨Q⟩ ⟨∙⟩ y∈⟨Q⟩ ∣ xy≈z)
+
+-- NOTE: the inclusion ⟨P⟩ ∩ ⟨Q⟩ ⊆ ⟨P ∩ Q⟩ does not hold for alle P and Q; let
+-- for example P = {S, K}, Q = {I}, then SKK = I ∈ ⟨P⟩ ∩ ⟨Q⟩, but P ∩ Q = ∅, and
+-- hence SKK = I ∉ P ∩ Q.
+-- TODO: formalise

Mockingbird/Forest/Combination/Properties.agda

@@ -0,0 +1,5 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination.Vec {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Mockingbird.Forest.Combination.Vec.Base forest public

Mockingbird/Forest/Combination/Vec.agda

@@ -0,0 +1,31 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination.Vec.Base {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Data.Fin using (Fin; zero; suc; #_)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Nat.Properties using (_≤?_)
+open import Data.Vec as Vec using (Vec; _∷_)
+open import Data.Vec.Relation.Unary.Any using (here; there) public
+open import Level using (_⊔_)
+open import Relation.Nullary.Decidable.Core using (True)
+open import Relation.Unary using (Pred; _∈_)
+
+open Forest forest
+
+import Mockingbird.Forest.Combination.Base forest as Base
+import Mockingbird.Forest.Combination.Properties forest as Combinationₚ
+open import Mockingbird.Forest.Combination.Base forest using ([_]; _⟨∙⟩_∣_; _⟨∙⟩_) public
+open import Data.Vec.Membership.Setoid setoid using () renaming (_∈_ to _∈′_)
+
+⟨_⟩ : ∀ {n} → Vec Bird n → Pred Bird (b ⊔ ℓ)
+⟨ bs ⟩ = Base.⟨ _∈′ bs ⟩
+  where
+
+[_]′ : ∀ {n} {bs : Vec Bird n} (i : Fin n) → Vec.lookup bs i ∈ ⟨ bs ⟩
+[_]′ {suc n} {x ∷ bs} zero = [ here refl ]
+[_]′ {suc n} {x ∷ bs} (suc i) = Combinationₚ.⟨ _ ⟩⊆⟨ _ ⟩ there [ i ]′
+
+[#_] : ∀ m {n} {m<n : True (suc m ≤? n)} {bs : Vec Bird n}
+  → Vec.lookup bs (#_ m {m<n = m<n}) ∈ ⟨ bs ⟩
+[# m ] = [ # m ]′

Mockingbird/Forest/Combination/Vec/Base.agda

@@ -0,0 +1,44 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Combination.Vec.Properties {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Data.Vec as Vec using (Vec; []; _∷_)
+import Data.Vec.Relation.Unary.Any as Any
+open import Function using (_$_; flip)
+open import Relation.Unary using (Pred; _∈_; _⊆_; ∅)
+
+open Forest forest
+
+open import Mockingbird.Forest.Combination.Vec.Base forest
+import Mockingbird.Forest.Combination.Properties forest as Combinationₚ
+
+subst : ∀ {n x y} {bs : Vec Bird n} → x ≈ y → x ∈ ⟨ bs ⟩ → y ∈ ⟨ bs ⟩
+subst = Combinationₚ.subst λ x≈y → Any.map (trans (sym x≈y))
+
+subst′ : ∀ {n x y} {bs : Vec Bird n} → y ≈ x → x ∈ ⟨ bs ⟩ → y ∈ ⟨ bs ⟩
+subst′ y≈x = subst (sym y≈x)
+
+⟨[]⟩ : ⟨ [] ⟩ ⊆ ∅
+⟨[]⟩ (X ⟨∙⟩ Y ∣ xy≈z) = ⟨[]⟩ X
+
+open import Mockingbird.Forest.Birds forest
+open import Mockingbird.Forest.Extensionality forest
+module _ ⦃ _ : Extensional ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasIdentity ⦄
+         ⦃ _ : HasThrush ⦄ ⦃ _ : HasKestrel ⦄ ⦃ _ : HasStarling ⦄ where
+  private
+    CI≈T : C ∙ I ≈ T
+    CI≈T = ext $ λ x → ext $ λ y → begin
+      C ∙ I ∙ x ∙ y  ≈⟨ isCardinal I x y ⟩
+      I ∙ y ∙ x      ≈⟨ ∙-congʳ $ isIdentity y ⟩
+      y ∙ x          ≈˘⟨ isThrush x y ⟩
+      T ∙ x ∙ y      ∎
+  
+  _ : T ∈  ⟨ C ∷ I ∷ [] ⟩
+  _ = subst CI≈T $ [# 0 ] ⟨∙⟩ [# 1 ]
+
+  _ : I ∈ ⟨ S ∷ K ∷ [] ⟩
+  _ = flip subst ([# 0 ] ⟨∙⟩ [# 1 ] ⟨∙⟩ [# 1 ]) $ ext $ λ x → begin
+    S ∙ K ∙ K ∙ x    ≈⟨ isStarling K K x ⟩
+    K ∙ x ∙ (K ∙ x)  ≈⟨ isKestrel x (K ∙ x) ⟩
+    x                ≈˘⟨ isIdentity x ⟩
+    I ∙ x            ∎

Mockingbird/Forest/Combination/Vec/Properties.agda

@@ -0,0 +1,42 @@
+open import Mockingbird.Forest using (Forest)
+
+module Mockingbird.Forest.Extensionality {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Algebra using (RightCongruent)
+open import Relation.Binary using (Rel; IsEquivalence; Setoid)
+open import Level using (_⊔_)
+
+open Forest forest
+
+-- TODO: if the arguments to the predicates is{Mockingbird,Thrush,Cardinal,...}
+-- are made implicit, then x can be implicit too.
+Similar : Rel Bird (b ⊔ ℓ)
+Similar A₁ A₂ = ∀ x → A₁ ∙ x ≈ A₂ ∙ x
+
+infix 4 _≋_
+_≋_ = Similar
+
+-- A forest is called extensional if similarity implies equality.
+IsExtensional : Set (b ⊔ ℓ)
+IsExtensional = ∀ {A₁ A₂} → A₁ ≋ A₂ → A₁ ≈ A₂
+
+-- A record to be used as an instance argument.
+record Extensional : Set (b ⊔ ℓ) where
+  field
+    ext : IsExtensional
+
+open Extensional ⦃ ... ⦄ public
+
+ext′ : ⦃ _ : Extensional ⦄ → ∀ {A₁ A₂} → (∀ {x} → A₁ ∙ x ≈ A₂ ∙ x) → A₁ ≈ A₂
+ext′ A₁≋A₂ = ext λ _ → A₁≋A₂
+
+-- Similarity is an equivalence relation.
+≋-isEquivalence : IsEquivalence _≋_
+≋-isEquivalence = record
+  { refl = λ _ → refl
+  ; sym = λ x≋y z → sym (x≋y z)
+  ; trans = λ x≋y y≋z w → trans (x≋y w) (y≋z w)
+  }
+
+≋-∙-congʳ : RightCongruent _≋_ _∙_
+≋-∙-congʳ {w} {x} {y} x≋y = λ _ → ∙-congʳ (x≋y w)

Mockingbird/Forest/Extensionality.agda

@@ -0,0 +1,326 @@
+open import Mockingbird.Forest using (Forest)
+
+-- To Mock a Mockingbird
+module Mockingbird.Problems.Chapter09 {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Data.Product using (_,_; proj₁; proj₂; ∃-syntax)
+open import Function using (_$_)
+open import Level using (_⊔_)
+open import Relation.Nullary using (¬_)
+
+open import Mockingbird.Forest.Birds forest
+
+open Forest forest
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
+  problem₁ : ∀ A → ∃[ B ] A IsFondOf B
+  problem₁ A =
+    let C = A ∘ M
+
+        isFond : A IsFondOf (C ∙ C)
+        isFond = sym $ begin
+          C ∙ C        ≈⟨ isComposition A M C ⟩
+          A ∙ (M ∙ C)  ≈⟨ ∙-congˡ (isMockingbird C) ⟩
+          A ∙ (C ∙ C)  ∎
+
+    in (C ∙ C , isFond)
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
+  problem₂ : ∃[ E ] IsEgocentric E
+  problem₂ =
+    let (E , isFond) = problem₁ M
+
+        isEgocentric : IsEgocentric E
+        isEgocentric = begin
+          E ∙ E  ≈˘⟨ isMockingbird E ⟩
+          M ∙ E  ≈⟨ isFond ⟩
+          E      ∎
+
+    in (E , isEgocentric)
+
+module _ ⦃ _ : HasComposition ⦄ (hasAgreeable : ∃[ A ] IsAgreeable A) where
+  A = proj₁ hasAgreeable
+  isAgreeable = proj₂ hasAgreeable
+
+  problem₃ : ∀ B → ∃[ C ] B IsFondOf C
+  problem₃ B =
+    let D = B ∘ A
+        (x , Ax≈Dx) = isAgreeable D
+
+        isFond : B IsFondOf (A ∙ x)
+        isFond = begin
+          B ∙ (A ∙ x)  ≈˘⟨ isComposition B A x ⟩
+          D ∙ x        ≈˘⟨ Ax≈Dx ⟩
+          A ∙ x        ∎
+
+    in (A ∙ x , isFond)
+
+-- Bonus question of Problem 3.
+C₂→HasAgreeable : ⦃ _ : HasMockingbird ⦄ → ∃[ A ] IsAgreeable A
+C₂→HasAgreeable = (M , λ B → (B , isMockingbird B))
+
+module _ ⦃ _ : HasComposition ⦄ (A B C : Bird) (Cx≈A[Bx] : IsComposition A B C) where
+  problem₄ : IsAgreeable C → IsAgreeable A
+  problem₄ C-isAgreeable D =
+    let E = D ∘ B
+        (x , Cx≈Ex) = C-isAgreeable E
+
+        agree : Agree A D (B ∙ x)
+        agree = begin
+          A ∙ (B ∙ x)  ≈˘⟨ Cx≈A[Bx] x ⟩
+          C ∙ x        ≈⟨ Cx≈Ex ⟩
+          E ∙ x        ≈⟨ isComposition D B x ⟩
+          D ∙ (B ∙ x)  ∎
+
+    in (B ∙ x , agree)
+
+module _ ⦃ _ : HasComposition ⦄ where
+  problem₅ : ∀ A B C → ∃[ D ] (∀ x → D ∙ x ≈ A ∙ (B ∙ (C ∙ x)))
+  problem₅ A B C =
+    let E = B ∘ C
+        D = A ∘ E
+    in (D , λ x → trans (isComposition A E x) $ ∙-congˡ (isComposition B C x))
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
+  problem₆ : ∀ A B → Compatible A B
+  problem₆ A B =
+    let C = A ∘ B
+        (y , Cy≈y) = problem₁ C
+        x = B ∙ y
+    in (x , y , trans (sym (isComposition A B y)) Cy≈y , refl)
+
+problem₇ : ∀ A → ∃[ B ] A IsFondOf B → IsHappy A
+problem₇ A (B , AB≈B) = (B , B , AB≈B , AB≈B)
+-- problem₇ : ∀ A → IsNormal A → IsHappy A
+
+module _ ⦃ _ : HasComposition ⦄ where
+  problem₈ : ∃[ H ] IsHappy H → ∃[ N ] IsNormal N
+  problem₈ (H , x , y , Hx≈y , Hy≈x) =
+    let N = H ∘ H
+
+        isFond : N IsFondOf x
+        isFond = begin
+          N ∙ x        ≈⟨ isComposition H H x ⟩
+          H ∙ (H ∙ x)  ≈⟨ ∙-congˡ Hx≈y ⟩
+          H ∙ y        ≈⟨ Hy≈x ⟩
+          x            ∎
+
+    in (N , x , isFond)
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasKestrel ⦄ where
+  problem₉ : ∃[ A ] IsHopelesslyEgocentric A
+  problem₉ =
+    let (A , KA≈A) = problem₁ K
+
+        isHopelesslyEgocentric : IsHopelesslyEgocentric A
+        isHopelesslyEgocentric x = begin
+          A ∙ x        ≈˘⟨ ∙-congʳ KA≈A ⟩
+          (K ∙ A) ∙ x  ≈⟨ isKestrel A x ⟩
+          A            ∎
+
+    in (A , isHopelesslyEgocentric)
+
+problem₁₀ : ∀ x y → x IsFixatedOn y → x IsFondOf y
+problem₁₀ x y xz≈y = xz≈y y
+
+problem₁₁ : ∀ K → IsKestrel K → IsEgocentric K → IsHopelesslyEgocentric K
+problem₁₁ K isKestrel KK≈K x = begin
+  K ∙ x        ≈˘⟨ ∙-congʳ KK≈K ⟩
+  (K ∙ K) ∙ x  ≈⟨ isKestrel K x ⟩
+  K            ∎
+
+problem₁₂ : ⦃ _ : HasKestrel ⦄ → ∀ x → IsEgocentric (K ∙ x) → K IsFondOf x
+problem₁₂ x [Kx][Kx]≈Kx = begin
+  K ∙ x              ≈˘⟨ [Kx][Kx]≈Kx ⟩
+  (K ∙ x) ∙ (K ∙ x)  ≈⟨ isKestrel x (K ∙ x) ⟩
+  x                  ∎
+
+problem₁₃ : ∀ A x y → IsHopelesslyEgocentric A → A ∙ x ≈ A ∙ y
+problem₁₃ A x y Az≈A = begin
+  A ∙ x  ≈⟨ Az≈A x ⟩
+  A      ≈˘⟨ Az≈A y ⟩
+  A ∙ y  ∎
+
+problem₁₄ : ∀ A x y → IsHopelesslyEgocentric A → (A ∙ x) ∙ y ≈ A
+problem₁₄ A x y Az≈A = begin
+  (A ∙ x) ∙ y  ≈⟨ ∙-congʳ (Az≈A x) ⟩
+  A ∙ y        ≈⟨ Az≈A y ⟩
+  A            ∎
+
+problem₁₅ : ∀ A x → IsHopelesslyEgocentric A → IsHopelesslyEgocentric (A ∙ x)
+problem₁₅ A x Az≈A y = begin
+  (A ∙ x) ∙ y  ≈⟨ ∙-congʳ (Az≈A x) ⟩
+  A ∙ y        ≈⟨ Az≈A y ⟩
+  A            ≈˘⟨ Az≈A x ⟩
+  A ∙ x        ∎
+
+problem₁₆ : ∀ K → IsKestrel K → ∀ x y → K ∙ x ≈ K ∙ y → x ≈ y
+problem₁₆ K isKestrel x y Kx≈Ky = begin
+  x            ≈˘⟨ isKestrel x K ⟩
+  -- NOTE: for the right-most kestrel, we can choose any bird. (Since we know
+  -- only of three birds to exist here, the only option is a combination of
+  -- {K, x, y}).
+  (K ∙ x) ∙ K  ≈⟨ ∙-congʳ Kx≈Ky ⟩
+  (K ∙ y) ∙ K  ≈⟨ isKestrel y K ⟩
+  y            ∎
+
+problem₁₇ : ∀ A x y → A IsFixatedOn x → A IsFixatedOn y → x ≈ y
+problem₁₇ A x y Az≈x Az≈y = begin
+  x      ≈˘⟨ Az≈x A ⟩
+  -- NOTE: for the right-most A, we can choose any bird. (In this case a
+  -- combination of {A, B, C}).
+  A ∙ A  ≈⟨ Az≈y A ⟩
+  y      ∎
+
+problem₁₈ : ⦃ _ : HasKestrel ⦄ → ∀ x → K IsFondOf K ∙ x → K IsFondOf x
+problem₁₈ x K[Kx]≈Kx = begin
+  K ∙ x              ≈˘⟨ isKestrel (K ∙ x) x ⟩
+  -- NOTE: for the right-most x, we can choose any bird.
+  (K ∙ (K ∙ x)) ∙ x  ≈⟨ ∙-congʳ K[Kx]≈Kx ⟩
+  (K ∙ x) ∙ x        ≈⟨ isKestrel x x ⟩
+  x                  ∎
+
+-- In the circumstances of Problem 19, the only bird in the forest is the
+-- kestrel.
+problem₁₉ : ∀ K → IsKestrel K → IsEgocentric K → ∀ x → x ≈ K
+problem₁₉ K isKestrel KK≈K x = begin
+  x            ≈⟨ lemma x x ⟩
+  K ∙ x        ≈˘⟨ ∙-congʳ KK≈K ⟩
+  (K ∙ K) ∙ x  ≈⟨ isKestrel K x ⟩
+  K            ∎
+  where
+    lemma : ∀ y z → y ≈ K ∙ z
+    lemma y z = begin
+      y                  ≈˘⟨ isKestrel y z ⟩
+      (K ∙ y) ∙ z        ≈˘⟨ ∙-congʳ (∙-congʳ KK≈K) ⟩
+      ((K ∙ K) ∙ y) ∙ z  ≈⟨ ∙-congʳ (isKestrel K y) ⟩
+      K ∙ z              ∎
+
+module _ ⦃ _ : HasIdentity ⦄ where
+  problem₂₀ : IsAgreeable I → ∀ A → ∃[ B ] A IsFondOf B
+  problem₂₀ isAgreeable A =
+    let (B , IB≈AB) = isAgreeable A
+
+        isFond : A IsFondOf B
+        isFond = begin
+          A ∙ B  ≈˘⟨ IB≈AB ⟩
+          I ∙ B  ≈⟨ isIdentity B ⟩
+          B      ∎
+
+    in (B , isFond)
+
+  problem₂₁ : (∀ A → ∃[ B ] A IsFondOf B) → IsAgreeable I
+  problem₂₁ isFond A =
+    let (B , AB≈B) = isFond A
+
+        agree : I ∙ B ≈ A ∙ B
+        agree = begin
+          I ∙ B  ≈⟨ isIdentity B ⟩
+          B      ≈˘⟨ AB≈B ⟩
+          A ∙ B  ∎
+
+    in (B , agree)
+
+  problem₂₂-1 : (∀ A B → Compatible A B) → ∀ A → IsNormal A
+  problem₂₂-1 compatible A =
+    let (x , y , Ix≈y , Ay≈x) = compatible I A
+
+        isFond : A IsFondOf y
+        isFond = begin
+          A ∙ y  ≈⟨ Ay≈x ⟩
+          x      ≈˘⟨ isIdentity x ⟩
+          I ∙ x  ≈⟨ Ix≈y ⟩
+          y      ∎
+    in (y , isFond)
+
+  problem₂₂-2 : (∀ A B → Compatible A B) → IsAgreeable I
+  problem₂₂-2 compatible A =
+    let (x , y , Ix≈y , Ay≈x) = compatible I A
+
+        agree : Agree I A y
+        agree = begin
+          I ∙ y  ≈⟨ isIdentity y ⟩
+          y      ≈˘⟨ Ix≈y ⟩
+          I ∙ x  ≈⟨ isIdentity x ⟩
+          x      ≈˘⟨ Ay≈x ⟩
+          A ∙ y  ∎
+
+    in (y , agree)
+
+  problem₂₃ : IsHopelesslyEgocentric I → ∀ x → I ≈ x
+  problem₂₃ isHopelesslyEgocentric x = begin
+    I      ≈˘⟨ isHopelesslyEgocentric x ⟩
+    I ∙ x  ≈⟨ isIdentity x ⟩
+    x      ∎
+
+module _ ⦃ _ : HasLark ⦄ ⦃ _ : HasIdentity ⦄ where
+  problem₂₄ : HasMockingbird
+  problem₂₄ = record
+    { M = L ∙ I
+    ; isMockingbird = λ x → begin
+        (L ∙ I) ∙ x  ≈⟨ isLark I x ⟩
+        I ∙ (x ∙ x)  ≈⟨ isIdentity (x ∙ x) ⟩
+        x ∙ x        ∎
+    }
+
+module _ ⦃ _ : HasLark ⦄ where
+  problem₂₅ : ∀ x → IsNormal x
+  problem₂₅ x =
+    let isFond : x IsFondOf (L ∙ x) ∙ (L ∙ x)
+        isFond = begin
+          x ∙ ((L ∙ x) ∙ (L ∙ x))  ≈˘⟨ isLark x (L ∙ x) ⟩
+          (L ∙ x) ∙ (L ∙ x)        ∎
+    in ((L ∙ x) ∙ (L ∙ x) , isFond)
+
+  problem₂₆ : IsHopelesslyEgocentric L → ∀ x → x IsFondOf L
+  problem₂₆ isHopelesslyEgocentric x = begin
+    x ∙ L        ≈˘⟨ ∙-congˡ $ isHopelesslyEgocentric L ⟩
+    x ∙ (L ∙ L)  ≈˘⟨ isLark x L ⟩
+    (L ∙ x) ∙ L  ≈⟨ ∙-congʳ $ isHopelesslyEgocentric x ⟩
+    L ∙ L        ≈⟨ isHopelesslyEgocentric L ⟩
+    L            ∎
+
+module _ ⦃ _ : HasLark ⦄ ⦃ _ : HasKestrel ⦄ where
+  problem₂₇ : L ≉ K → ¬ L IsFondOf K
+  problem₂₇ L≉K isFond =
+    let K-fondOf-KK : K IsFondOf K ∙ K
+        K-fondOf-KK = begin
+          K ∙ (K ∙ K)              ≈˘⟨ ∙-congʳ isFond ⟩
+          (L ∙ K) ∙ (K ∙ K)        ≈⟨ isLark K (K ∙ K) ⟩
+          K ∙ ((K ∙ K) ∙ (K ∙ K))  ≈⟨ ∙-congˡ $ isKestrel K (K ∙ K) ⟩
+          K ∙ K                    ∎
+
+        isEgocentric : IsEgocentric K
+        isEgocentric = problem₁₈ K K-fondOf-KK
+
+        L≈K : L ≈ K
+        L≈K = problem₁₉ K isKestrel isEgocentric L
+
+    in L≉K L≈K
+
+  problem₂₈ : K IsFondOf L → ∀ x → x IsFondOf L
+  problem₂₈ KL≈L =
+    let isHopelesslyEgocentric : IsHopelesslyEgocentric L
+        isHopelesslyEgocentric y = begin
+          L ∙ y        ≈˘⟨ ∙-congʳ KL≈L ⟩
+          (K ∙ L) ∙ y  ≈⟨ isKestrel L y ⟩
+          L            ∎
+    in problem₂₆ isHopelesslyEgocentric
+
+module _ ⦃ _ : HasLark ⦄ where
+  problem₂₉ : ∃[ x ] IsEgocentric x
+  problem₂₉ =
+    let (y , [LL]y≈y) = problem₂₅ (L ∙ L)
+
+        isEgocentric : IsEgocentric (y ∙ y)
+        isEgocentric = begin
+          (y ∙ y) ∙ (y ∙ y)  ≈˘⟨ isLark (y ∙ y) y ⟩
+          (L ∙ (y ∙ y)) ∙ y  ≈˘⟨ ∙-congʳ (isLark L y) ⟩
+          ((L ∙ L) ∙ y) ∙ y  ≈⟨ ∙-congʳ [LL]y≈y ⟩
+          y ∙ y              ∎
+
+        -- The expression of yy in terms of L and brackets.
+        _  : y ∙ y ≈ ((L ∙ (L ∙ L)) ∙ (L ∙ (L ∙ L))) ∙ ((L ∙ (L ∙ L)) ∙ (L ∙ (L ∙ L)))
+        _ = refl
+
+    in (y ∙ y , isEgocentric)

Mockingbird/Problems/Chapter09.agda

@@ -0,0 +1,53 @@
+open import Mockingbird.Forest using (Forest)
+
+-- Is There a Sage Bird?
+module Mockingbird.Problems.Chapter10 {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Data.Product using (_,_; proj₁; proj₂; ∃-syntax)
+open import Function using (_$_)
+
+open import Mockingbird.Forest.Birds forest
+
+open Forest forest
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasLark ⦄ where
+  private
+    hasMockingbirdComposer : ∃[ A ] (∀ x y → A ∙ x ∙ y ≈ x ∙ (M ∙ y))
+    hasMockingbirdComposer = (L , isMockingbirdComposer)
+      where
+        isMockingbirdComposer = λ x y → begin
+          L ∙ x ∙ y    ≈⟨ isLark x y ⟩
+          x ∙ (y ∙ y)  ≈˘⟨ ∙-congˡ $ isMockingbird y ⟩
+          x ∙ (M ∙ y)  ∎
+
+  hasSageBird : HasSageBird
+  hasSageBird = record
+    { Θ = M ∘ L
+    ; isSageBird = λ x → begin
+        x ∙ ((M ∘ L) ∙ x)        ≈⟨ ∙-congˡ $ isComposition M L x ⟩
+        x ∙ (M ∙ (L ∙ x))        ≈⟨ ∙-congˡ $ isMockingbird (L ∙ x) ⟩
+        x ∙ ((L ∙ x) ∙ (L ∙ x))  ≈˘⟨ isLark x (L ∙ x) ⟩
+        (L ∙ x) ∙ (L ∙ x)        ≈˘⟨ isMockingbird (L ∙ x) ⟩
+        M ∙ (L ∙ x)              ≈˘⟨ isComposition M L x ⟩
+        (M ∘ L) ∙ x              ∎
+    }
+
+module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄
+         (hasMockingbirdComposer : ∃[ A ] (∀ x y → A ∙ x ∙ y ≈ x ∙ (M ∙ y))) where
+
+  private
+    A = proj₁ hasMockingbirdComposer
+    [Ax]y≈x[My] = proj₂ hasMockingbirdComposer
+
+    instance
+      hasLark : HasLark
+      hasLark = record
+        { L = A
+        ; isLark = λ x y → begin
+            (A ∙ x) ∙ y  ≈⟨ [Ax]y≈x[My] x y ⟩
+            x ∙ (M ∙ y)  ≈⟨ ∙-congˡ $ isMockingbird y ⟩
+            x ∙ (y ∙ y)  ∎
+        }
+
+  hasSageBird′ : HasSageBird
+  hasSageBird′ = hasSageBird

Mockingbird/Problems/Chapter10.agda

@@ -0,0 +1,225 @@
+open import Mockingbird.Forest using (Forest)
+
+-- A Gallery of Sage Birds
+module Mockingbird.Problems.Chapter13 {b ℓ} (forest : Forest {b} {ℓ}) where
+
+open import Function using (_$_)
+open import Data.Product using (proj₂)
+
+open import Mockingbird.Forest.Birds forest
+import Mockingbird.Problems.Chapter09 forest as Chapter₉
+import Mockingbird.Problems.Chapter10 forest as Chapter₁₀
+import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
+import Mockingbird.Problems.Chapter12 forest as Chapter₁₂
+
+open Forest forest
+
+problem₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasRobin ⦄ → HasSageBird
+problem₁ = record
+  { Θ = B ∙ M ∙ (R ∙ M ∙ B)
+  ; isSageBird = λ x → begin
+      x ∙ (B ∙ M ∙ (R ∙ M ∙ B) ∙ x)  ≈⟨ ∙-congˡ lemma ⟩
+      x ∙ (M ∙ (B ∙ x ∙ M))          ≈⟨ isFond ⟩
+      M ∙ (B ∙ x ∙ M)                ≈˘⟨ lemma ⟩
+      B ∙ M ∙ (R ∙ M ∙ B) ∙ x        ∎
+  } where
+  isFond = λ {x} → proj₂ (Chapter₁₁.problem₂ x)
+
+  lemma : ∀ {x} → B ∙ M ∙ (R ∙ M ∙ B) ∙ x ≈ M ∙ (B ∙ x ∙ M)
+  lemma {x} = begin
+    B ∙ M ∙ (R ∙ M ∙ B) ∙ x  ≈⟨ isBluebird M (R ∙ M ∙ B) x ⟩
+    M ∙ (R ∙ M ∙ B ∙ x)      ≈⟨ ∙-congˡ $ isRobin M B x ⟩
+    M ∙ (B ∙ x ∙ M)          ∎
+
+problem₂ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasCardinal ⦄ → HasSageBird
+problem₂ = record
+  { Θ = B ∙ M ∙ (C ∙ B ∙ M)
+  ; isSageBird = λ x → begin
+      x ∙ (B ∙ M ∙ (C ∙ B ∙ M) ∙ x)  ≈⟨ ∙-congˡ lemma ⟩
+      x ∙ (M ∙ (B ∙ x ∙ M))          ≈⟨ isFond ⟩
+      M ∙ (B ∙ x ∙ M)                ≈˘⟨ lemma ⟩
+      B ∙ M ∙ (C ∙ B ∙ M) ∙ x        ∎
+  } where
+  isFond = λ {x} → proj₂ (Chapter₁₁.problem₂ x)
+
+  lemma : ∀ {x} → B ∙ M ∙ (C ∙ B ∙ M) ∙ x ≈ M ∙ (B ∙ x ∙ M)
+  lemma {x} = begin
+    B ∙ M ∙ (C ∙ B ∙ M) ∙ x  ≈⟨ isBluebird M (C ∙ B ∙ M) x ⟩
+    M ∙ (C ∙ B ∙ M ∙ x)      ≈⟨ ∙-congˡ $ isCardinal B M x ⟩
+    M ∙ (B ∙ x ∙ M)          ∎
+
+problem₃ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasLark ⦄ → HasSageBird
+problem₃ = record
+  { Θ = B ∙ M ∙ L
+  ; isSageBird = isSageBird ⦃ Chapter₁₀.hasSageBird ⦄
+  } where instance hasComposition = Chapter₁₁.problem₁
+
+problem₄ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasBluebird ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
+problem₄ = record
+  { Θ = B ∙ M ∙ (B ∙ W ∙ B)
+  ; isSageBird = isSageBird ⦃ problem₃ ⦄
+  } where instance hasLark = Chapter₁₂.problem₃
+
+problem₆ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasLark ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
+problem₆ = record
+  { Θ = W ∙ (Q ∙ L ∙ (Q ∙ L))
+  ; isSageBird = λ x → begin
+      x ∙ (W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x)  ≈⟨ ∙-congˡ lemma ⟩
+      x ∙ (L ∙ x ∙ (L ∙ x))            ≈⟨ isFond ⟩
+      L ∙ x ∙ (L ∙ x)                  ≈˘⟨ lemma ⟩
+      W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x        ∎
+  } where
+  isFond = λ {x} → proj₂ (Chapter₉.problem₂₅ x)
+
+  lemma : ∀ {x} → W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x ≈ L ∙ x ∙ (L ∙ x)
+  lemma {x} = begin
+      W ∙ (Q ∙ L ∙ (Q ∙ L)) ∙ x  ≈⟨ isWarbler (Q ∙ L ∙ (Q ∙ L)) x ⟩
+      Q ∙ L ∙ (Q ∙ L) ∙ x ∙ x    ≈⟨ ∙-congʳ $ isQueerBird L (Q ∙ L) x ⟩
+      Q ∙ L ∙ (L ∙ x) ∙ x        ≈⟨ isQueerBird L (L ∙ x) x ⟩
+      L ∙ x ∙ (L ∙ x)            ∎
+  
+
+problem₅ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasCardinal ⦄ ⦃ _ : HasWarbler ⦄ → HasSageBird
+problem₅ = problem₆
+  where
+    instance
+      hasQueerBird = Chapter₁₁.problem₃₇′
+      hasLark = Chapter₁₂.problem₃
+
+problem₇ = problem₅
+
+problem₈ : ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasQueerBird ⦄ → HasSageBird
+problem₈ = record
+  { Θ = Q ∙ (Q ∙ M) ∙ M
+  ; isSageBird = λ x → sym $ begin
+      Q ∙ (Q ∙ M) ∙ M ∙ x        ≈⟨ isQueerBird (Q ∙ M) M x ⟩
+      M ∙ (Q ∙ M ∙ x)            ≈⟨ isMockingbird (Q ∙ M ∙ x) ⟩
+      Q ∙ M ∙ x ∙ (Q ∙ M ∙ x)    ≈⟨ isQueerBird M x (Q ∙ M ∙ x) ⟩
+      x ∙ (M ∙ (Q ∙ M ∙ x))      ≈˘⟨ ∙-congˡ $ isQueerBird (Q ∙ M) M x ⟩
+      x ∙ (Q ∙ (Q ∙ M) ∙ M ∙ x)  ∎
+  }
+
+-- TODO: formalise regularity.
+
+problem₉ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasLark ⦄ → HasSageBird
+problem₉ = record
+  { Θ = S ∙ L ∙ L
+  ; isSageBird = λ x → begin
+      x ∙ (S ∙ L ∙ L ∙ x)    ≈⟨ ∙-congˡ $ isStarling L L x ⟩
+      x ∙ (L ∙ x ∙ (L ∙ x))  ≈⟨ isFond ⟩
+      L ∙ x ∙ (L ∙ x)        ≈˘⟨ isStarling L L x ⟩
+      S ∙ L ∙ L ∙ x          ∎
+  } where
+  isFond = λ {x} → proj₂ (Chapter₉.problem₂₅ x)
+
+problem₁₀ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasWarbler ⦄ ⦃ _ : HasStarling ⦄ → HasSageBird
+problem₁₀ = record
+  { Θ = W ∙ S ∙ (B ∙ W ∙ B)
+  ; isSageBird = λ x → begin
+      x ∙ (W ∙ S ∙ (B ∙ W ∙ B) ∙ x) ≈⟨⟩
+      x ∙ (W ∙ S ∙ L ∙ x)      ≈⟨ ∙-congˡ $ ∙-congʳ $ isWarbler S L ⟩
+      x ∙ (S ∙ L ∙ L ∙ x)      ≈⟨ isSageBird ⦃ problem₉ ⦄ x ⟩
+      S ∙ L ∙ L ∙ x            ≈˘⟨ ∙-congʳ $ isWarbler S L ⟩
+      W ∙ S ∙ L ∙ x            ≈⟨⟩
+      W ∙ S ∙ (B ∙ W ∙ B) ∙ x  ∎
+  } where instance hasLark = Chapter₁₂.problem₃
+
+problem₁₁ : ⦃ _ : HasBluebird ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasThrush ⦄ → HasTuringBird
+problem₁₁ = record
+  { U = B ∙ (B ∙ W ∙ (C ∙ B)) ∙ M
+  ; isTuringBird = λ x y → begin
+      B ∙ (B ∙ W ∙ (C ∙ B)) ∙ M ∙ x ∙ y  ≈⟨ ∙-congʳ $ isBluebird (B ∙ W ∙ (C ∙ B)) M x ⟩
+      B ∙ W ∙ (C ∙ B) ∙ (M ∙ x) ∙ y      ≈⟨ ∙-congʳ $ isBluebird W (C ∙ B) (M ∙ x) ⟩
+      W ∙ (C ∙ B ∙ (M ∙ x)) ∙ y          ≈⟨ isWarbler (C ∙ B ∙ (M ∙ x)) y ⟩
+      C ∙ B ∙ (M ∙ x) ∙ y ∙ y            ≈⟨ ∙-congʳ $ isCardinal B (M ∙ x) y ⟩
+      B ∙ y ∙ (M ∙ x) ∙ y                ≈⟨ isBluebird y (M ∙ x) y ⟩
+      y ∙ (M ∙ x ∙ y)                    ≈⟨ ∙-congˡ $ ∙-congʳ $ isMockingbird x ⟩
+      y ∙ (x ∙ x ∙ y)                    ∎
+  } where
+  instance
+    hasCardinal = Chapter₁₁.problem₂₁′
+    hasLark = Chapter₁₂.problem₇
+
+problem₁₂ : ⦃ _ : HasTuringBird ⦄ → HasSageBird
+problem₁₂ = record
+  { Θ = U ∙ U
+  ; isSageBird = λ x → sym $ isTuringBird U x
+  }
+
+problem₁₃ : ⦃ _ : HasQueerBird ⦄ ⦃ _ : HasWarbler ⦄ → HasOwl
+problem₁₃ = record
+  { O = Q ∙ Q ∙ W
+  ; isOwl = λ x y → begin
+      Q ∙ Q ∙ W ∙ x ∙ y  ≈⟨ ∙-congʳ $ isQueerBird Q W x ⟩
+      W ∙ (Q ∙ x) ∙ y    ≈⟨ isWarbler (Q ∙ x) y ⟩
+      Q ∙ x ∙ y ∙ y      ≈⟨ isQueerBird x y y ⟩
+      y ∙ (x ∙ y)        ∎
+  }
+
+problem₁₄ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasLark ⦄ → HasTuringBird
+problem₁₄ = record
+  { U = L ∙ O
+  ; isTuringBird = λ x y → begin
+      L ∙ O ∙ x ∙ y    ≈⟨ ∙-congʳ $ isLark O x ⟩
+      O ∙ (x ∙ x) ∙ y  ≈⟨ isOwl (x ∙ x) y ⟩
+      y ∙ (x ∙ x ∙ y)  ∎
+  }
+
+problem₁₅ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasIdentity ⦄ → HasMockingbird
+problem₁₅ = record
+  { M = O ∙ I
+  ; isMockingbird = λ x → begin
+      O ∙ I ∙ x    ≈⟨ isOwl I x ⟩
+      x ∙ (I ∙ x)  ≈⟨ ∙-congˡ $ isIdentity x ⟩
+      x ∙ x        ∎
+  }
+
+problem₁₆ : ⦃ _ : HasStarling ⦄ ⦃ _ : HasIdentity ⦄ → HasOwl
+problem₁₆ = record
+  { O = S ∙ I
+  ; isOwl = λ x y → begin
+      S ∙ I ∙ x ∙ y    ≈⟨ isStarling I x y ⟩
+      I ∙ y ∙ (x ∙ y)  ≈⟨ ∙-congʳ $ isIdentity y ⟩
+      y ∙ (x ∙ y)      ∎
+  }
+
+problem₁₇ : ∀ x y → x IsFondOf y → x IsFondOf x ∙ y
+problem₁₇ x y xy≈y = begin
+  x ∙ (x ∙ y)  ≈⟨ ∙-congˡ xy≈y ⟩
+  x ∙ y        ∎
+
+problem₁₈ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → IsSageBird (O ∙ Θ)
+problem₁₈ x = begin
+  x ∙ (O ∙ Θ ∙ x)    ≈⟨ ∙-congˡ $ isOwl Θ x ⟩
+  x ∙ (x ∙ (Θ ∙ x))  ≈⟨ isFond ⟩
+  x ∙ (Θ ∙ x)        ≈˘⟨ isOwl Θ x ⟩
+  O ∙ Θ ∙ x          ∎
+  where
+    isFond : x IsFondOf (x ∙ (Θ ∙ x))
+    isFond = problem₁₇ x (Θ ∙ x) (isSageBird x)
+
+problem₁₉ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → IsSageBird (Θ ∙ O)
+problem₁₉ x = sym $ begin
+  Θ ∙ O ∙ x        ≈˘⟨ ∙-congʳ $ isSageBird O ⟩
+  O ∙ (Θ ∙ O) ∙ x  ≈⟨ isOwl (Θ ∙ O) x ⟩
+  x ∙ (Θ ∙ O ∙ x)  ∎
+
+problem₂₀ : ⦃ _ : HasOwl ⦄ → ∀ A → O IsFondOf A → IsSageBird A
+problem₂₀ A OA≈A x = begin
+  x ∙ (A ∙ x)  ≈˘⟨ isOwl A x ⟩
+  O ∙ A ∙ x    ≈⟨ ∙-congʳ OA≈A ⟩
+  A ∙ x        ∎
+
+problem₂₁ : ⦃ _ : HasSageBird ⦄ → ∀ A → IsChoosy A → IsSageBird (Θ ∙ A)
+problem₂₁ A isChoosy = isChoosy (Θ ∙ A) $ isSageBird A
+
+open import Mockingbird.Forest.Extensionality forest
+
+problem₂₂ : ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → O ∙ Θ ≋ Θ
+problem₂₂ x = begin
+  O ∙ Θ ∙ x    ≈⟨ isOwl Θ x ⟩
+  x ∙ (Θ ∙ x)  ≈⟨ isSageBird x ⟩
+  Θ ∙ x        ∎
+
+problem₂₃ : ⦃ _ : Extensional ⦄ ⦃ _ : HasOwl ⦄ ⦃ _ : HasSageBird ⦄ → O IsFondOf Θ
+problem₂₃ = ext problem₂₂

Mockingbird/Problems/Chapter11.agda

@@ -0,0 +1,10 @@
+# Explorations in combinatory logic with Agda
+
+Contents:
+- A formalisation in [Agda](https://wiki.portal.chalmers.se/agda/Main/HomePage) of the
+  theory and problems of *To Mock a Mockingbird* by Raymond Smullyan.
+- A formalisation in Agda of [Haskell Curry's](https://en.wikipedia.org/wiki/Haskell_Curry)
+  thesis *Grundlagen der Kombinatorischen Logik*. See [part 1](https://www.jstor.org/stable/2370619)
+  and [part 2](https://www.jstor.org/stable/2370716).
+
+Both are work in progress.

Mockingbird/Problems/Chapter12.agda

@@ -0,0 +1,3 @@
+name: combinatory-logic
+include: .
+depend: standard-library

Mockingbird/Problems/Chapter13.agda

@@ -0,0 +1,27 @@
+module index where
+
+-- A formalisation of Haskell B. Curry’s thesis Grundlagen der Kombinatorischen
+-- Logik. See <https://www.jstor.org/stable/2370619> (part 1) and
+-- <https://www.jstor.org/stable/2370716> (part 2).
+import CombinatoryLogic.Equality
+import CombinatoryLogic.Forest
+import CombinatoryLogic.Semantics
+import CombinatoryLogic.Syntax
+
+-- A formalisation of the theory and problems presented in To Mock a Mockingbird
+-- by Raymond Smullyan.
+import Mockingbird.Forest
+import Mockingbird.Forest.Base
+import Mockingbird.Forest.Birds
+import Mockingbird.Forest.Combination
+import Mockingbird.Forest.Combination.Base
+import Mockingbird.Forest.Combination.Properties
+import Mockingbird.Forest.Combination.Vec
+import Mockingbird.Forest.Combination.Vec.Base
+import Mockingbird.Forest.Combination.Vec.Properties
+import Mockingbird.Forest.Extensionality
+import Mockingbird.Problems.Chapter09
+import Mockingbird.Problems.Chapter10
+import Mockingbird.Problems.Chapter11
+import Mockingbird.Problems.Chapter12
+import Mockingbird.Problems.Chapter13