BirdPromotions.agda

open import Relation.Binary.PropositionalEquality renaming (refl to definition-chasing)
open ≡-Reasoning
open import Agda.Builtin.String
open import Function

defn-chasing : ∀ {i} {A : Set i} (x : A) → String → A → A
defn-chasing x reason supposedly-x-again = supposedly-x-again

syntax defn-chasing x reason xish = x ≡⟨ reason ⟩′ xish
infixl 3 defn-chasing

_even-under_ : ∀ {A B : Set} → {x y : A} → x ≡ y → (P : A → B) → P x ≡ P y
x≡y even-under P = cong P x≡y

data BirdList (A : Set) : Set where
  [] : BirdList A
  [_] : A → BirdList A
  _++_ : BirdList A → BirdList A → BirdList A

K : {A B : Set} → A → B → A
K x _ = x

_★_ : {A B : Set} → (A → B) → BirdList A → BirdList B
_ ★ [] = []
f ★ [ a ] = [ f a ]
f ★ (x ++ y) = (f ★ x) ++ (f ★ y)

★-empty
  : ∀ {A B : Set}
  → (f : A → B)
  → (f ★_) ∘ K [] ≗ K []
★-empty f x = 
  begin
    ((f ★_) ∘ K []) x
  ≡⟨ "defn of composition" ⟩′
    (f ★_) (K [] x)
  ≡⟨ "defn of K" ⟩′
    (f ★_) []
  ≡⟨ "application" ⟩′
    f ★ []
  ≡⟨ "defn of map" ⟩′
    []
  ≡⟨ "defn of K" ⟩′
    K [] x
  ∎