-- A wip formalisation of the ninth chapter of "To Mock a Mockingbird"
-- $Id: mockingbird.agda,v 1.2 2024/10/21 15:12:46 oc45ujef Exp $
open import Data.Product
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

record Forest {ℓ} (Bird : Set ℓ) : Set ℓ where
  infix 5 _$_
  infix 6 _∘_
  
  field
    _$_ : Bird → Bird → Bird
    
    C₁ : ∀ (A B : Bird) → Σ Bird λ C → ∀ (x : Bird) → C $ x ≡ A $ (B $ x)
    
  _∘_ : Bird → Bird → Bird
  A ∘ B = proj₁ (C₁ A B)

  ∘-condition : (A B : Bird) → (x : Bird) → (A ∘ B) $ x ≡ A $ (B $ x)
  ∘-condition A B = proj₂ (C₁ A B)
  
  _isfondof_ : Bird → Bird → Set ℓ
  A isfondof B = A $ B ≡ B

  egocentric : Bird → Set ℓ
  egocentric B = B isfondof B

  _agreeswith_on_ : Bird → Bird → Bird → Set ℓ
  A agreeswith B on x = A $ x ≡ B $ x

  agreeable : Bird → Set ℓ
  agreeable A = ∀ (B : Bird) → Σ Bird λ x → A agreeswith B on x

  compatible : (A B : Bird) → Set ℓ
  compatible A B = Σ Bird λ x → Σ Bird λ y → A $ x ≡ y × B $ y ≡ x

  happy : Bird → Set ℓ
  happy A = compatible A A

module _ {ℓ} {Bird : Set ℓ} (f : Forest Bird) where
  open Forest f

  record HasMockingbird : Set ℓ where
    field
      C₂ : Σ Bird λ M → ∀ (x : Bird) → M $ x ≡ x $ x
    M = proj₁ C₂
    Mocking = proj₂ C₂

  record HasAgreeable : Set ℓ where
    field
      C₃ : Σ Bird agreeable

    Ag = proj₁ C₃
    agrees = proj₂ C₃

module _ {ℓ} {Bird : Set ℓ} (f : Forest Bird) (m : HasMockingbird f) where
  open Forest f
  open HasMockingbird m
  -- 1. every bird is fond of at least one bird
  fondness-lemma : ∀ (A : Bird) → Σ Bird λ B → A isfondof B
  fondness-lemma A = ((A ∘ M) $ A ∘ M) , sym (trans (∘-condition A M (A ∘ M)) (cong (A $_) (Mocking (A ∘ M))))

  -- 2. at least one bird is egocentric
  egocentric-lemma : Σ Bird egocentric
  egocentric-lemma = let (C , H) = fondness-lemma M in
    C , trans (sym (Mocking C)) H

  -- any two birds are compatible
  compatibility-lemma : ∀ (A B : Bird) → compatible A B
  compatibility-lemma A B = (M $ ((B ∘ A) ∘ M)) , (A $ (M $ (B ∘ A) ∘ M)) , refl ,
    (begin B $ (A $ (M $ (B ∘ A) ∘ M))
      ≡⟨ sym (∘-condition B A (M $ (B ∘ A) ∘ M)) ⟩
        B ∘ A $ (M $ (B ∘ A) ∘ M)
      ≡⟨ sym (∘-condition (B ∘ A) M ((B ∘ A) ∘ M)) ⟩
        (B ∘ A) ∘ M $ (B ∘ A) ∘ M
      ≡⟨ sym (Mocking ((B ∘ A) ∘ M)) ⟩
        M $ (B ∘ A) ∘ M ∎)
  
module _ {ℓ} {Bird : Set ℓ} (f : Forest Bird) (a : HasAgreeable f) where
  open Forest f
  open HasAgreeable a

  -- 3. Every bird is fond of at least one bird
  fondness-lemma₂ : ∀ (A : Bird) → Σ Bird λ B → A isfondof B
  fondness-lemma₂ A = let (C , H) = agrees (A ∘ Ag) in (Ag $ C) , sym (trans H (∘-condition A Ag C))

module _ {ℓ} {Bird : Set ℓ} (f : Forest Bird) where
  open Forest f

  -- 3. Mockingbirds are agreeable
  bonus : HasMockingbird f → HasAgreeable f
  bonus m = record { C₃ = M , λ B → B , Mocking B }
    where open HasMockingbird m

  -- 4.
  agreeable-compose : ∀ (A B : Bird) → agreeable (A ∘ B) → agreeable A
  agreeable-compose A B ag x = let (D , H) = ag (x ∘ B) in B $ D ,
    (begin A $ (B $ D)
      ≡⟨ sym (∘-condition A B D) ⟩
        A ∘ B $ D
      ≡⟨ H ⟩
        x ∘ B $ D
      ≡⟨ ∘-condition x B D ⟩
    x $ (B $ D) ∎)

  -- 5.
  compose₂ : ∀ (A B C : Bird) → Σ Bird λ D → ∀ (x : Bird) → D $ x ≡ A $ (B $ (C $ x))
  compose₂ A B C = (A ∘ (B ∘ C)) , λ x → trans (∘-condition A (B ∘ C) x) (cong (A $_) (∘-condition B C x))

  -- 7.
  fond-happy : ∀ (A : Bird) → Σ Bird (A isfondof_) → happy A
  fond-happy A (B , f) = B , B , f , f