open import Data.Nat hiding (fold)
open import Data.Fin hiding (fold ; lift )
open import Data.Product
open import Data.Sum
open import Data.Unit

open import Relation.Binary.PropositionalEquality

open import Logic.Logic
open import Logic.IProp 
open import Level renaming (zero to zeroL ; suc to sucL)
open Logic.IProp.Applicative {zeroL}

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.InitialAlgebra
open import IDesc.Lifting
open import IDesc.Induction

open import Orn.Ornament.Examples.Lifting hiding () renaming (□h to □ho)
open import Orn.Ornament

module Orn.AlgebraicOrnament.Coherence
           {K : Set }
           {X : K  Set }
           (D : func  K K)
           (α :  D ⟧func X  X) where

open import Orn.AlgebraicOrnament
open import Orn.Ornament.Algebra {u = proj₁} (algOrn D α)
open import Orn.Ornament.CartesianMorphism

forgetAlgOrn : ∀{k x}  μ (algOrnD D α) (k , x)  μ D k
forgetAlgOrn = forget

-- Thanks to Andrea Vezzosi for the proof!

-- Paper: Remark 4.21
coherentOrn : ∀{k x}  
                (t : μ (algOrnD D α) (k , x))  
                 x  fold D α (forget t)
coherentOrn = induction (algOrnD D α) P
                         {i}{xs}  step {i} {xs})

    where P : {kx : Σ K X}  μ (algOrnD D α) kx  Set 
          P {(k , x)} t =  x  fold D α (forget t)

          step' : (kx : Σ K X)
                  (D' : IDesc  K)
                  (α' :  D'  X  X (proj₁ kx)) 
                  let algOrnD' : IDesc  (Σ K X)
                      algOrnD' =  Desc.algOrnD (proj₁ kx) (proj₂ kx) D' α' in
                  (xs :  algOrnD'  (μ (algOrnD D α))) 
                  □h algOrnD'  {kx} t   proj₂ kx  fold D α  (forget t)) xs 
                   proj₁ xs  Fold.hyps D α D' 
                                           (forgetOrnNT (algOrn D α) (□ho D' (proj₁ xs))
                                             (Fold.hyps (algOrnD D α) forgetAlg  □ho D' (proj₁ xs) ⟧Orn  (proj₂ (proj₂ xs))))
          step' (k , x) (`var i) α' (xs , q , xxs) ih = ih
          step' (k , x) `1  α' (tt , q , tt) tt = pf refl
          step' (k , x) (D₁  D₂)  α' 
                ((xs₁ , xs₂) , q  , xxs₁ , xxs₂) (ih₁ , ih₂) = 
                cong₂  x y  (x , y)) <$>
                  step' (k , x) D₁  xs₁  α' (xs₁ , xs₂)) (xs₁ , q , xxs₁) ih₁  
                  step' (k , x) D₂  xs₂  α' (xs₁ , xs₂)) (xs₂ , q , xxs₂) ih₂
          step' (k , x) ( n T)  α' ((s , xs) , q , xxs) ih = 
                cong⊢  x  s , x) 
                      (step' (k , x) (T s)  xs  α' (s , xs)) (xs , q , xxs) ih)
          step' (k , x) ( S T)  α' ((s , xs) , q , xxs) ih = 
                cong⊢  x  s , x) 
                      (step' (k , x) (T s)  xs  α' (s , xs)) (xs , q , xxs) ih)
          step' (k , .(α' f)) ( S T)  α' (f , refl , xxs) ih = 
                extensionality  s  
                  step' (k , α' f) (T s)  xs  α' f ) (f s , refl , (xxs s)) (ih s))

          step : DAlg (algOrnD D α) P
          step {(k , .(α xs))} {(xs , refl , xxs)} ih =
            cong⊢ α (step' (k , α xs) 
                           (func.out D k) (α {k}) 
                           ((xs , refl ,  xxs)) ih)