-- Code supplement for Case Study on Bushes
-- (C) 2020 Patricia Johann, Andrew Polonsky
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0.

module Bush where

open import Agda.Primitive
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
open import Function
open import Agda.Builtin.Nat
open import Agda.Builtin.List

data bigUnit {l} : Set l where
    bigtt : bigUnit

{-# NO_POSITIVITY_CHECK #-}
data Bush {l} : Set l → Set l where
  Bnil  : ∀ {A} → Bush A
  Bcons : ∀ {A} → A → Bush (Bush A) → Bush A

module Predicates where
  -- This section defines predicate lifting of Bushes, which will be used
  -- in formulating the deep induction rules.

  -- Pred X is the type of predicates on X valued in the l'th universe.
  Pred : ∀ {l} → Set → Set _
  Pred {l} X = X → Set l

  -- The type of morphisms between predicates with the same domain.
  Pred-map : ∀ {l} {X : Set} → Pred {l} X → Pred {l} X → Set _
  Pred-map P1 P2 = ∀ x → P1 x → P2 x

  -- The constantly true predicate
  K₁ : ∀ {l} {A} → Pred {l} A
  K₁ = λ _ → bigUnit

  K : ∀ {A} → Pred {lzero} A
  K {A} = λ _ → A

-----------------------------------------------------------------------------------------------
  -- The plain induction rule for bushes
  Bind : ∀ {l} (P : ∀ (X : Set) → Bush X → Set l)
                → (∀ X → P X Bnil)
                → (∀ X → (x : X) → (b : Bush (Bush X)) → (P (Bush X) b) → P X (Bcons x b) )
                → ∀ X → (b : Bush X) → P X b
  Bind P Pnil Pcons X Bnil = Pnil X
  Bind P Pnil Pcons X (Bcons x bbx) = Pcons X x bbx (Bind P Pnil Pcons (Bush X) bbx)
-----------------------------------------------------------------------------------------------

  -- Lifting of predicates on A to predicates on Bush A
  {-# TERMINATING #-}
  Bush^ : ∀ {l₀ l} {X : Set l₀} → (X → Set l) → (Bush X → Set l)
  Bush^ {l₀} {l} {X} Y Bnil = bigUnit
  Bush^ {l₀} {l} {X} Y (Bcons x b) = Y x × Bush^ (Bush^ Y) b

  -- Lifting also acts on morphisms between predicates with the same carrier
  {-# TERMINATING #-}
  Bush^-map : ∀ {l} {X : Set} {Q1 Q2 : X → Set l}
              → Pred-map {l} Q1 Q2 → Pred-map (Bush^ Q1) (Bush^ Q2)
  Bush^-map Q12 Bnil q = bigtt
  Bush^-map Q12 (Bcons x b) (y , bby) =
                Q12 x y , Bush^-map (Bush^-map Q12) b bby

  -- Lifting preserves truth
  {-# TERMINATING #-}
  Bush^-K₁ : ∀ {l} {X} (b : Bush X) → Bush^ {lzero} {l} K₁ b
  Bush^-K₁ Bnil = bigtt
  Bush^-K₁ (Bcons x b) = bigtt , Bush^-map {Q1 = K₁} (const ∘ Bush^-K₁) b (Bush^-K₁ b)

  {-# TERMINATING #-}
  Bush^-K : ∀ {X} (b : Bush X) → Bush^ K b
  Bush^-K Bnil = bigtt
  Bush^-K (Bcons x b) = x , Bush^-map {Q1 = K} (const ∘ Bush^-K) b (Bush^-K b)
  -- Bush^-K (Bcons x b) = x , Bush^-map {Q1 = K₁} (const ∘ Bush^-K) b (Bush^-K₁ b)

  -- "Dependent Bush^-map".  Important for the next development.
  Bush^-dmap : ∀ {l} {X : Set} {Xp : X → Set l} → (∀ x → Xp x) → ∀ bx → Bush^ Xp bx
  Bush^-dmap f bx = Bush^-map (λ x _ → f x) bx (Bush^-K₁ bx)

  -- If a predicate is always true (has a section), then so is its lifting.
  Bush^-truth : ∀ {l} {X} {Xp : X → Set l} → (∀ x → Xp x) → ∀ bx → Bush^ Xp bx
  Bush^-truth {X = A} {B} H ba = Bush^-map (const ∘ H) ba (Bush^-K₁ ba)

open Predicates

module Bush-Ind where
  -- Induction Principles for Bush

  -- Part 1.  Naive induction rules.

  -- The most basic, non-polymorphic, non-deep, non-mutually recursive
  -- induction principle for Bushes.
  -- Not very useful for proving facts about the datatype.
  Bind₀ : ∀ (P : ∀ (X : Set) → Bush X → Set)
            → (∀ (X : Set) → P X Bnil)
            → (∀ (X : Set) → (x : X) → (b : Bush (Bush X))
                 → (P (Bush X) b) → P X (Bcons x b) )
            → ∀ (X : Set) → (b : Bush X) → P X b
  Bind₀ P Pnil Pcons X Bnil = Pnil X
  Bind₀ P Pnil Pcons X (Bcons x bbx) = Pcons X x bbx (Bind₀ P Pnil Pcons (Bush X) bbx)

  -- Like the above, but works for predicates valued in an arbitrary higher universe.
  Bind₁ : ∀ {l} (P : ∀ (X : Set) → Bush X → Set l)
                → (∀ X → P X Bnil)
                → (∀ X → (x : X) → (b : Bush (Bush X))
                     → (P (Bush X) b) → P X (Bcons x b) )
                → ∀ X → (b : Bush X) → P X b
  Bind₁ P Pnil Pcons X Bnil = Pnil X
  Bind₁ P Pnil Pcons X (Bcons x bbx) = Pcons X x bbx (Bind₁ P Pnil Pcons (Bush X) bbx)

  -- Mutual induction. Still terminating, still not very powerful.
  Bind₂ : ∀ {l} (P : ∀ (X : Set) → Bush X → Set l)
                (Q : ∀ (X : Set) → Bush X → Set l)
                → (∀ X → P X Bnil )
                → (∀ X (x : X) (b : Bush (Bush X)) → Q (Bush X) b → P X (Bcons x b) )
                → (∀ X → Q X Bnil )
                → (∀ X (x : X) (b : Bush (Bush X)) → P (Bush X) b → Q X (Bcons x b) )
                → ∀ X (b : Bush X) → P X b × Q X b
  Bind₂ P Q Pnil Pcons Qnil Qcons X Bnil = Pnil X , Qnil X
  Bind₂ P Q Pnil Pcons Qnil Qcons X (Bcons x b) =
    let rec = Bind₂ P Q Pnil Pcons Qnil Qcons (Bush X) b
     in Pcons X x b (snd rec) , Qcons X x b (fst rec)

  -- A variant of the above with product distributed over the abstractions
  -- in the conclusion of the rule.
  Bind₂-× : ∀ {l} (P : ∀ (X : Set) → Bush X → Set l)
                  (Q : ∀ (X : Set) → Bush X → Set l)
                  → (∀ X → P X Bnil )
                  → (∀ X (x : X) (b : Bush (Bush X)) → Q (Bush X) b → P X (Bcons x b) )
                  → (∀ X → Q X Bnil )
                  → (∀ X (x : X) (b : Bush (Bush X)) → P (Bush X) b → Q X (Bcons x b) )
                  → (∀ X b → P X b) × (∀ X b → Q X b)
  Bind₂-× P Q Pnil Pcons Qnil Qcons =
    let aux = Bind₂ P Q Pnil Pcons Qnil Qcons
     in (λ X b → fst (aux X b)) , (λ X b → snd (aux X b))
     -- (λ X b → fst (Bind₂ P Q Pnil Pcons Qnil Qcons X b)) ,
     -- (λ X b → snd (Bind₂ P Q Pnil Pcons Qnil Qcons X b))

  -- Part 2.  Deep induction rules.

  -- Deep induction.
  -- Terminating and not really useful yet.
  BDind₀ : ∀ {l} (P : ∀ (X : Set) (Y : X → Set l)→ Bush X → Set l)
                 → (∀ X Y → P X Y Bnil )
                 → (∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
                    → P (Bush X) (Bush^ Y) bbx → P X Y (Bcons x bbx) )
                 → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  BDind₀ P Pnil Pcons X Y Bnil by = Pnil X Y
  BDind₀ P Pnil Pcons X Y (Bcons x bbx) (y , bby) =
     Pcons X Y x bbx y (BDind₀ P Pnil Pcons (Bush X) (Bush^ Y) bbx bby)


-----------------------------------------------------------------------------------------------
  -- A variant of the above in which the predicate in the induction hypothesis
  -- is updated from (Bush^ Y) to (P X Y).
  -- This is the "natural" deep induction principle for Bushes.
  -- However, it is no longer terminating.
  {-# TERMINATING #-}
  BDind₁ : ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
                 → (∀ X Y → P X Y Bnil )
                 → (∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
                    → P (Bush X) (P X Y) bbx → P X Y (Bcons x bbx) )
                 → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  BDind₁ P Pnil Pcons X Y Bnil by = Pnil X Y
  BDind₁ P Pnil Pcons X Y (Bcons x bbx) (y , bby) =
    Pcons X Y x bbx y (BDind₁ P Pnil Pcons (Bush X) (P X Y) bbx
                        (Bush^-map (BDind₁ P Pnil Pcons X Y) bbx bby) )

  -- We define the deep induction rule to be the one with hypothesis P (Bush X) (P X Y).
  BDind = BDind₁
-----------------------------------------------------------------------------------------------


-- Another variant, where the hypothesis (P (Bush X) (P X Y) bbx)
  -- is split into (P (Bush X) (Bush^ Y) bbx) and (Bush^ (P X Y) bbx).
  -- Basically, this principle is "half-way" between the previous two.
  {-# TERMINATING #-}
  BDind₂ : ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
                 → (∀ X Y → P X Y Bnil )
                 → (∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
                    → P (Bush X) (Bush^ Y) bbx → Bush^ (P X Y) bbx → P X Y (Bcons x bbx) )
                 → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  BDind₂ P Pnil Pcons X Y Bnil by = Pnil X Y
  BDind₂ P Pnil Pcons X Y (Bcons x bbx) (y , bby) =
    Pcons X Y x bbx y (BDind₂ P Pnil Pcons (Bush X) (Bush^ Y) bbx bby)
                      (Bush^-map {Q1 = Bush^ Y} (BDind₂ P Pnil Pcons X Y) bbx bby)


  -- The first deep induction rule implies the last one provided a certain
  -- "lifting property" of the given predicate.
  BDind₀⇒BDind₂ :
     ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
         → (Plift : ∀ X (Y : X → Set l) → Pred-map (P (Bush X) (Bush^ Y)) (Bush^ (P X Y) ))
         → (Pnil : ∀ X Y → P X Y Bnil )
         → (Pcons : ∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
            → P (Bush X) (Bush^ Y) bbx → Bush^ (P X Y) bbx → P X Y (Bcons x bbx) )
         → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  BDind₀⇒BDind₂ P Plift Pnil Pcons
    = BDind₀ (λ X Y b → P X Y b)
             (λ X Y → Pnil X Y)
             (λ X Y x bbx y pby → Pcons X Y x bbx y pby (Plift X Y bbx pby))

  -- The same "lifting property" also allows us to derive BDind₂ from the
  -- vanilla "shallow" structural induction principle.
  Bind₁⇒BDind₂ :
     ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
         → (Plift : ∀ X (Y : X → Set l) → Pred-map (P (Bush X) (Bush^ Y)) (Bush^ (P X Y) ))
         → (Pnil : ∀ X Y → P X Y Bnil )
         → (Pcons : ∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
            → P (Bush X) (Bush^ Y) bbx → Bush^ (P X Y) bbx → P X Y (Bcons x bbx) )
         → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  Bind₁⇒BDind₂ {l} P Plift Pnil Pcons A B ba bb =
    Bind₁ (λ X b → ∀ (Y : X → Set l) → Bush^ Y b → P X Y b)
          (λ X Y bigtt → Pnil X Y)
          (λ X x bbx H Y → λ {(y , bby) → Pcons X Y x bbx y (H (Bush^ Y) bby)
                                            (Plift X Y bbx (H (Bush^ Y) bby))})
          A ba B bb

  -- However, the same lifting property does not suffice to get back the primary rule,
  -- as the following (incomplete) proof demonstrates.
  -- BDind₂⇒BDind₁ :
  --    ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
  --        → (Plift : ∀ X (Y : X → Set l) → Pred-map (P (Bush X) (Bush^ Y)) (Bush^ (P X Y) ))
  --        → (Pnil : ∀ X Y → P X Y Bnil )
  --        → (Pcons : ∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
  --           → P (Bush X) (P X Y) bbx → P X Y (Bcons x bbx) )
  --           -- → P (Bush X) (Bush^ Y) bbx → Bush^ (P X Y) bbx → P X Y (Bcons x bbx) )
  --        → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  -- BDind₂⇒BDind₁ P Plift Pnil Pcons A B ba bb
  --   = BDind₂ (λ X Y b → P X Y b)
  --            (λ X Y → Pnil X Y)
  --            (λ X Y x bbx y pby bpy →
  --              (Pcons X Y x bbx y {! Plift X Y bbx pby   !}))
  --            A B ba bb

  -- The primary deep induction rule implies BDind₂ if we assume functoriality of P.
  BDind₁⇒BDind₂ :
    ∀ {l} (P : ∀ X (Y : X → Set l)→ Bush X → Set l)
        → (Pmap : ∀ X (Y1 Y2 : X → Set l) → Pred-map Y1 Y2 → Pred-map (P X Y1) (P X Y2) )
        → (Pnil : ∀ X Y → P X Y Bnil )
        → (Pcons : ∀ X Y (x : X) (bbx : Bush (Bush X)) (y : Y x)
           → P (Bush X) (Bush^ Y) bbx → Bush^ (P X Y) bbx → P X Y (Bcons x bbx) )
        → ∀ A (B : A → Set l) (ba : Bush A) → Bush^ B ba → P A B ba
  BDind₁⇒BDind₂ P Pmap Pnil Pcons A B ba bb
   = fst (BDind₁ (λ X Y b → P X Y b × Bush^ Y b)
                 (λ X Y → Pnil X Y , bigtt)
                 (λ X Y x bbx y → λ { (ppby , bpby) →
                   Pcons X Y x bbx y (Pmap (Bush X) _ _ (λ _ → snd) bbx ppby)
                                     (Bush^-map (λ _ → proj₁) bbx bpby)
                   , (y , Bush^-map (λ _ → snd) bbx bpby ) })
                 A B ba bb )

  -- Mutual deep induction.  Pcons takes P (Bush X) (Q X Y) as IH.
  {-# TERMINATING #-}
  BDind₃ : ∀ {l} (P : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
                 (Q : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
                 (Pnil : ∀ X Y → P X Y Bnil )
                 (Qnil : ∀ X Y → Q X Y Bnil )
                 (Pcons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → P X Y (Bcons x bbx) )
                 (Qcons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → Q X Y (Bcons x bbx) )
                 → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
  BDind₃ P Q Pnil Qnil Pcons Qcons X Y Bnil bigtt = Pnil X Y , Qnil X Y
  BDind₃ P Q Pnil Qnil Pcons Qcons X Y (Bcons x b) (y , bby) =
    let rec = BDind₃ P Q Pnil Qnil Pcons Qcons
     in (Pcons X Y x b y (fst (rec (Bush X) (Q X Y) b
          (Bush^-map (λ bx by → snd (rec X Y bx by)) b bby)))) ,
        (Qcons X Y x b y (snd (rec (Bush X) (P X Y) b
          (Bush^-map (λ bx by → fst (rec X Y bx by)) b bby))))

  -- Mutual deep induction.  Pcons takes Q (Bush X) (P X Y) as IH.
  {-# TERMINATING #-}
  BDind₄ : ∀ {l} (P : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
                 (Q : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
                 (Pnil : ∀ X Y → P X Y Bnil )
                 (Qnil : ∀ X Y → Q X Y Bnil )
                 (Pcons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → P X Y (Bcons x bbx) )
                 (Qcons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → Q X Y (Bcons x bbx) )
                 → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
  BDind₄ P Q Pnil Qnil Pcons Qcons X Y Bnil bigtt = Pnil X Y , Qnil X Y
  BDind₄ P Q Pnil Qnil Pcons Qcons X Y (Bcons x b) (y , bby) =
    let rec = BDind₄ P Q Pnil Qnil Pcons Qcons
     in (Pcons X Y x b y (snd (rec (Bush X) (P X Y) b
          (Bush^-map (λ bx by → fst (rec X Y bx by)) b bby)))) ,
        (Qcons X Y x b y (fst (rec (Bush X) (Q X Y) b
          (Bush^-map (λ bx by → snd (rec X Y bx by)) b bby))))

  BDind₁⇒BDind₃ : ∀ {l}
    (P : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
    (Q : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
    (Pmap : ∀ {X} {Y1 Y2 : X → Set l} → Pred-map Y1 Y2 → Pred-map (P X Y1) (P X Y2) )
    (Qmap : ∀ {X} {Y1 Y2 : X → Set l} → Pred-map Y1 Y2 → Pred-map (Q X Y1) (Q X Y2) )
    (Pnil : ∀ X Y → P X Y Bnil )
    (Qnil : ∀ X Y → Q X Y Bnil )
    (Pcons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → P X Y (Bcons x bbx) )
    (Qcons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → Q X Y (Bcons x bbx) )
     → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
  BDind₁⇒BDind₃ P Q Pmap Qmap Pnil Qnil Pcons Qcons =
    BDind₁ (λ X Y b → P X Y b × Q X Y b)
           (λ X Y → Pnil X Y , Qnil X Y)
           (λ X Y x bbx y → λ {(ppqy , qpqy) →
                Pcons X Y x bbx y (Pmap (λ _ → snd) bbx ppqy)
              , Qcons X Y x bbx y (Qmap (λ _ → fst) bbx qpqy) })

  BDind₁⇒BDind₄ : ∀ {l}
    (P : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
    (Q : ∀ (X : Set) → (X → Set l) → Bush X → Set l)
    (Pmap : ∀ {X} {Y1 Y2 : X → Set l} → Pred-map Y1 Y2 → Pred-map (P X Y1) (P X Y2) )
    (Qmap : ∀ {X} {Y1 Y2 : X → Set l} → Pred-map Y1 Y2 → Pred-map (Q X Y1) (Q X Y2) )
    (Pnil : ∀ X Y → P X Y Bnil )
    (Qnil : ∀ X Y → Q X Y Bnil )
    (Pcons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → P X Y (Bcons x bbx) )
    (Qcons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → Q X Y (Bcons x bbx) )
     → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
  BDind₁⇒BDind₄ P Q Pmap Qmap Pnil Qnil Pcons Qcons =
    BDind₁ (λ X Y b → P X Y b × Q X Y b)
           (λ X Y → Pnil X Y , Qnil X Y)
           (λ X Y x bbx y → λ {(ppqy , qpqy) →
                Pcons X Y x bbx y (Qmap (λ _ → fst) bbx qpqy)
              , Qcons X Y x bbx y (Pmap (λ _ → snd) bbx ppqy) })

open Bush-Ind

module MapsAndFolds where

  -- The plain, vanilla map for Bushes.
  -- Unsatisfactory because the inner recursive call is unguarded
  -- (uses the entire function being defined), hence cannot be
  -- derived by an induction combinator.
  {-# TERMINATING #-}
  Bmap₀ : ∀ {l} {X Y : Set l} → (X → Y) → Bush X → Bush Y
  Bmap₀ f Bnil = Bnil
  Bmap₀ f (Bcons x b) = Bcons (f x) (Bmap₀ (Bmap₀ f) b)


-----------------------------------------------------------------------------------------------
-- The plain, non-dependent fold for Bushes.
  -- Unsatisfactory for two reasons:
  -- 1. Its definition depends on Bmap.
  -- 2. It's not obviously terminating, hence cannot be seen
  -- as a specialization of induction to non-dependent predicates.
  {-# TERMINATING #-}
  Bfold₀ : ∀ {l} (F : Set l → Set l)
            → (∀ (X : Set l) → F X)
            → (∀ (X : Set l) → X → F (F X) → F X)
            → ∀ X → Bush X → F X
  Bfold₀ F Fnil Fcons X Bnil = Fnil X
  Bfold₀ F Fnil Fcons X (Bcons x bbx) = Fcons X x (Bfold₀ F Fnil Fcons (F X)
                                                  (Bmap₀ (Bfold₀ F Fnil Fcons X) bbx))

  Bfold = Bfold₀
-----------------------------------------------------------------------------------------------

-- Map defined polymorphically from the above fold.
  -- It is terminating, but it does use polymorphism in an essential way.
  -- (And indirectly depends on the earlier map via its occurrence in the fold.)
  -- As a result, there's a mismatch in universe indices.
  Bfmap₁ : ∀ {l} {A : Set (lsuc l)} {B : Set l} → (A → B) → Bush A → Bush B
  Bfmap₁ {l} {A} {B} f ba = Bfold₀ (λ X → ∀ Y → (X → Y) → Bush Y)
                              (λ X Y f → Bnil)
                              (λ X x p Y f → Bcons (f x) (p (Bush Y) (λ y → y Y f)))
                              A ba B f

  -- The following fold uses an additional hypothesis on F (asserting that it is a functor)
  -- so as to avoid using Bmap.  It is equivalent to Bfold by naturality.
  -- (Essentially it is "going the other way through the square".)
  -- However, it is still non-terminating, because it applies Fmap
  -- to an unguarded recursive call.
  {-# TERMINATING #-}
  Bfold₂ : ∀ (F : Set₁ → Set₁)
           → (Fmap : ∀ {X Y : Set₁} → (X → Y) → F X → F Y)
           → (∀ X → F X)
           → (∀ X → X → F (F X) → F X)
           → ∀ X → Bush X → F X
  Bfold₂ F Fmap Fnil Fcons A Bnil = Fnil A
  Bfold₂ F Fmap Fnil Fcons A (Bcons x bbx) =
    Fcons A x (Fmap (Bfold₂ F Fmap Fnil Fcons A)
                    (Bfold₂ F Fmap Fnil Fcons (Bush A) bbx))
  -- Bfold₂ F Fmap Fnil Fcons A ba = Bind₁ (const ∘ F) (Fnil)
  --       (λ A x bbx fbx → Fcons A x (Fmap (Bfold₂ F Fmap Fnil Fcons _) fbx)) A ba

  -- Map defined polymorphically from the above fold.
  -- As the previous version, but providing an instance to the new Fmap hypothesis.
  Bfmap₂ : ∀ {A} {B} → (A → B) → Bush A → Bush B
  Bfmap₂ {A} {B} f ba = Bfold₂ (λ X → ∀ Y → (X → Y) → Bush Y)
                              (λ f H Y g → H Y (g ∘ f))
                              (λ X Y f → Bnil)
                              (λ X x p Y f → Bcons (f x) (p (Bush Y) (λ y → y Y f)))
                              A ba B f

  -- A version of the plain recursive fold for a universe-polymorphic functor.
  {-# TERMINATING #-}
  Bfold₃ : ∀ (F : ∀ {l} → Set l → Set l)
            → (∀ (X : Set) → F X)
            → (∀ (X : Set) → X → F (F X) → F X)
            → ∀ X → Bush X → F X
  Bfold₃ F Fnil Fcons X Bnil = Fnil X
  Bfold₃ F Fnil Fcons X (Bcons x bbx) =
    Fcons X x (Bfold₃ F Fnil Fcons (F X) (Bmap₀ (Bfold₃ F Fnil Fcons X) bbx))

  -- Bfold with polymorphic definition of Bmap inlined into it,
  -- to try to break the mutual dependency.
  -- This only works with type-in-type.  (And still no termination guarantee.)
  -- {-# TERMINATING #-}
  -- Bfold₄ : ∀ F
  --          → (∀ X → F X)
  --          → (∀ X → X → F (F X) → F X)
  --          → ∀ X → Bush X → F X
  -- Bfold₄ F Fnil Fcons X Bnil = Fnil X
  -- Bfold₄ F Fnil Fcons X (Bcons x bbx) =
  --   Fcons X x (Bfold₄ F Fnil Fcons (F X)
  --                     (Bfold₄ (λ X → ∀ Y → (X → Y) → Bush Y)
  --                             (λ X Y f → Bnil)
  --                             (λ X x p Y f → Bcons (f x) (p (Bush Y) (λ y → y Y f)))
  --                             _ bbx _ (Bfold₄ F Fnil Fcons X)))

  Lift-from-fun : ∀ {l} {X : Set} {Y : Set l} (bx : Bush X)
                  → (X → Y) → Bush^ (λ _ → Y) bx
  Lift-from-fun {X} {Y} bx f = Bush^-map (const ∘ f) bx (Bush^-K₁ bx)


-----------------------------------------------------------------------------------------------
-- The following definition of Bmap is satisfactory because it is derived directly
  -- from the (deep) induction rule. It is obtained by sufficiently restricting the
  -- polymorphic Bmap-predicate relative to a given predicate on the underlying type.
  -- Specifically, instead of asking for a function from X to Z to create an element
  -- of Bush Z, we prove by induction that, if one can get to Z from any data element of
  -- b : Bush X satisfying the given predicate Y, then one can get to Bush Z.
  Bmap : ∀ {A B : Set} → (A → B) → Bush A → Bush B
  Bmap {A} {B} f ba =
    let P : ∀ X → (X → Set₁) → (Bush X → Set₁)
        P X Y b = ∀ Z → Bush^ (λ x → Y x → Z) b → Bush Z
        N : ∀ X Y → P X Y Bnil
        N X Y = λ Z h → Bnil
        C : ∀ X Y x bbx → Y x → P (Bush X) (P X Y) bbx → P X Y (Bcons x bbx)
        C X Y x bbx y h = λ {Z (v , bbl) →
            Bcons (v y) (h (Bush Z) (Bush^-map (λ bx bl bp → bp Z bl) bbx bbl))}
     in BDind₁ P N C A K₁ ba (Bush^-K₁ ba) B (Lift-from-fun ba (const ∘ f))
-----------------------------------------------------------------------------------------------


  -- Not really a map or a fold, but a related combinator needed for later developments.
  Bzipwith : ∀ {A B C : Set} → (A → B → C) → Bush A → Bush B → Bush C
  Bzipwith {A} {B} {C} f ba bb =
   let P : ∀ X → (X → Set₁) → Bush X → Set₁
       P X Xp b = ∀ (Y Z : Set) → Bush^ (λ x → Xp x → Y → Z) b → Bush Y → Bush Z
       Pnil : ∀ X Xp → P X Xp Bnil
       Pnil = λ X Xp Y Z b by → Bnil
       Pcons : ∀ X Xp x bbx → Xp x → P (Bush X) (P X Xp) bbx → P X Xp (Bcons x bbx)
       Pcons = λ X Xp x bbx px ppx →
         λ { Y Z (f' , bbf') Bnil          → Bnil
           ; Y Z (f' , bbf') (Bcons y bby) → Bcons (f' px y)
               (ppx (Bush Y) (Bush Z) (Bush^-map (λ bx fa H by → H Y Z fa by) bbx bbf' ) bby) }
    in BDind₁ P Pnil Pcons A K₁ ba (Bush^-K₁ ba) B C (Lift-from-fun ba (const ∘ f)) bb

  -- For illustration, the same proof does NOT work with plain induction:
  -- a crucial hypothesis is missing.
  -- Bzipwith₀ : ∀ {A B C} → (A → B → C) → Bush A → Bush B → Bush C
  -- Bzipwith₀ {A} {B} {C} f ba bb =
  --   let P : ∀ X → Pred (Bush X)
  --       P X b = ∀ Y Z → Bush^ (λ x → Y → Z) b → Bush Y → Bush Z
  --    -- P X Xp b = ∀ Y Z → Bush^ (λ x → Xp x → Y → Z) b → Bush Y → Bush Z
  --       Pnil : ∀ X → P X Bnil
  --       Pnil = λ X Y Z b by → Bnil
  --       Pcons : ∀ X x bbx → P (Bush X) bbx → P X (Bcons x bbx)
  --       Pcons = λ X x bbx ppx →
  --         λ { Y Z (f' , bbf') Bnil          → Bnil
  --           ; Y Z (f' , bbf') (Bcons y bby) → Bcons (f' y)
  --               (ppx (Bush Y) (Bush Z) (Bush^-map (λ bx fa by → {!   !}) bbx bbf' ) bby) }
  --            -- (ppx (Bush Y) (Bush Z) (Bush^-map (λ bx fa H by → H Y Z fa by) bbx bbf' ) bby) }
  --    in Bind₁ P Pnil Pcons A ba B C (Lift-from-fun ba f) bb

  Bpair : ∀ {A B} → Bush A → Bush B → Bush (A × B)
  Bpair = Bzipwith _,_

  Bapp : ∀ {A B} → Bush (A → B) → Bush A → Bush B
  Bapp = Bzipwith id


open MapsAndFolds

module EqualityLaws where

  data _≡_ {l} {A : Set l} : A → A → Set l where
    refl : ∀ {a : A} → a ≡ a

-----------------------------------------------------------------------------------------------
  Bind-in-id : ∀ X b → Bind₀ (λ X _ → Bush X) (λ X → Bnil) (λ X x bbx _ → Bcons x bbx) X b ≡ b
  Bind-in-id =
    Bind₀ (λ X b → Bind₀ (λ X _ → Bush X) (λ X → Bnil) (λ X x bbx _ → Bcons x bbx) X b ≡ b)
          (λ _ → refl) (λ x b _ _ → refl)
-----------------------------------------------------------------------------------------------


  Bcons-≡ : ∀ {l} {A : Set l} → {a1 a2 : A} → a1 ≡ a2 → {b1 b2 : Bush (Bush A)} → b1 ≡ b2
            → Bcons a1 b1 ≡ Bcons a2 b2
  Bcons-≡ refl refl = refl

  pair-≡ : ∀ {l} {A : Set l} {a1 a2 : A} → a1 ≡ a2 →
           ∀ {m} {B : Set m} {b1 b2 : B} → b1 ≡ b2
           → (a1 , b1) ≡ (a2 , b2)
  pair-≡ refl refl = refl

  app-≡ : ∀ {l} {m} {A : Set l} {B : Set m} (f : A → B) {a1 a2 : A} → a1 ≡ a2 → f a1 ≡ f a2
  app-≡ f refl = refl

  tran : ∀ {l} {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  tran refl refl = refl

  _≃_ : ∀ {l m} {A : Set l} {B : Set m} → (A → B) → (A → B) → Set _
  f ≃ g = ∀ a → f a ≡ g a

  refl-≃ : ∀ {l m} {A : Set l} {B : Set m} → ∀ (f : A → B) → f ≃ f
  refl-≃ f a = refl

  {-# TERMINATING #-}
  Bush^-map-≃ : ∀ {l} {X : Set} {Y1 Y2 : X → Set l} {f1 f2 : Pred-map Y1 Y2}
                → (∀ x → f1 x ≃ f2 x) → ∀ bx → Bush^-map f1 bx ≃ Bush^-map f2 bx
  Bush^-map-≃ {l} {X} {Y1} {Y2} {f1} {f2} eq Bnil bigtt = refl
  Bush^-map-≃ {l} {X} {Y1} {Y2} {f1} {f2} eq (Bcons x bbx) (y , bby) =
    pair-≡ (eq x y) (Bush^-map-≃ (Bush^-map-≃ eq) bbx bby)

  {-# TERMINATING #-}
  Bush^-map-∘ : ∀ {l} {X : Set} {Q1 Q2 Q3 : X → Set l}
                → (q12 : Pred-map Q1 Q2) (q23 : Pred-map Q2 Q3) (bx : Bush X)
                → (Bush^-map q23 bx ∘ Bush^-map q12 bx) ≃ Bush^-map (λ x → q23 x ∘ q12 x) bx
  Bush^-map-∘ {l} {X} {Q1} {Q2} {Q3} q12 q23 Bnil bigtt = refl
  Bush^-map-∘ {l} {X} {Q1} {Q2} {Q3} q12 q23 (Bcons x bbx) (q , bbq) =
    pair-≡ refl (tran (Bush^-map-∘ (Bush^-map q12) (Bush^-map q23) bbx bbq)
                      (Bush^-map-≃ (Bush^-map-∘ q12 q23) bbx bbq))

  Lift-from-fun-≃ : ∀ {l} {A B : Set} {C : Set l} {f g : A → B} (e : f ≃ g) → ∀ (ba : Bush A)
                  → Lift-from-fun ba (λ x (c : C) → f x) ≡ Lift-from-fun ba (const ∘ g)
  Lift-from-fun-≃ e Bnil = refl
  Lift-from-fun-≃ e (Bcons x ba) = pair-≡ (app-≡ const (e x))
                (Bush^-map-≃ (Bush^-map-≃ λ x y → app-≡ const (e x) ) ba
                  (Bush^-map (λ x _ → Bush^-K₁ x) ba (Bush^-K₁ ba)))

  Bmap-Pred : ∀ (X : Set) → (X → Set₁) → (Bush X → Set₁)
  Bmap-Pred X Y b = ∀ (Z : Set) → Bush^ (λ x → Y x → Z) b → Bush Z
  Bmap-Nil : ∀ X Y → Bmap-Pred X Y Bnil
  Bmap-Nil X Y = λ Z h → Bnil
  Bmap-Cons : ∀ X Y x bbx → Y x
          → Bmap-Pred (Bush X) (Bmap-Pred X Y) bbx → Bmap-Pred  X Y (Bcons x bbx)
  Bmap-Cons X Y x bbx y h = λ {Z (v , bbl) →
      Bcons (v y) (h (Bush Z) (Bush^-map (λ bx bl bp → bp Z bl) bbx bbl))}

  Bmap-≃ : ∀ {A B} (f g : A → B) → f ≃ g → Bmap f ≃ Bmap g
  Bmap-≃ {A} {B} f g e ba =
    app-≡ (BDind₁ {lsuc lzero} Bmap-Pred Bmap-Nil Bmap-Cons A K₁ ba (Bush^-K₁ ba) B)
          (Lift-from-fun-≃ {lsuc lzero} {A} {B} {bigUnit} {f} {g} e ba)


  -- The fact that Bush^-map maps id to id is proved by deep induction.
  Bush^-map-id : ∀ {l} {X : Set} {P : X → Set l} (φ : Pred-map P P)
                 → (∀ x → φ x ≃ id) → (∀ {bx} → Bush^-map φ bx ≃ id)
  Bush^-map-id {l} {A} {PA} φ₀ H₀ {bx₀} px₀ =
    BDind₁ {lsuc l} (λ X Y bx → ∀ (P : X → Set l) (φ : Pred-map P P)
                       → (∀ x → Y x → φ x ≃ id) → Bush^-map φ bx ≃ id)
            (λ X Y P φ H → λ { bigtt → refl })
            (λ X Y x bbx y IH P φ H → λ { (p , bbp) → pair-≡ (H x y p)
              (IH (Bush^ P) (Bush^-map φ) (λ bx hp z → hp P φ H z) bbp) })
            A K₁ bx₀ (Bush^-K₁ bx₀) PA φ₀ (λ x → const (H₀ x)) px₀

  -- Bush^ can itself be defined by deep induction.
  Bush^₁ : ∀ {l} {X : Set} → (X → Set l) → (Bush X → Set l)
  Bush^₁ {l} {X₀} Y₀ bx₀ =
    BDind {lsuc l} (λ X Y bx → (∀ x → Y x → Set l) → Set l)
          (λ X Y Z → bigUnit)
          (λ X Y x bbx y IH Z → Z x y × IH (λ bx bZ → bZ Z))
          X₀ K₁ bx₀ (Bush^-K₁ bx₀) (const ∘ Y₀)

  -- Bush^-map can also be defined by deep induction.
  Bush^-map₀ : ∀ {l} {X : Set} {Q1 Q2 : X → Set l}
               → Pred-map Q1 Q2 → Pred-map (Bush^ Q1) (Bush^ Q2)
  Bush^-map₀ {l} {X₀} {Q₁} {Q₂} Q₁₂ bx₀ bq₀ =
    BDind {lsuc l} (λ X Y bx → ∀ (Q1 Q2 : X → Set l)
                      → (∀ x → Y x → Q1 x → Q2 x) → Bush^ Q1 bx → Bush^ Q2 bx)
          (λ X Y Q1 Q2 H bigtt → bigtt)
          (λ X Y x bbx y IH Q1 Q2 Q12 → λ { (q , bbq) → Q12 x y q ,
              IH (Bush^ Q1) (Bush^ Q2) (λ bx ξ bq → ξ Q1 Q2 Q12 bq) bbq } )
          X₀ K₁ bx₀ (Bush^-K₁ bx₀) Q₁ Q₂ (const ∘ Q₁₂) bq₀

open EqualityLaws