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
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)