open import Chapter5.Container

module Chapter8.Container.Morphism.Contornament.Composition.Vertical
         {I J K L M N : Set}
         {u₂₁ : K → I}{v₂₁ : L → J}
         {u₃₂ : M → K}{v₃₂ : N → L}
         {φ₁ : I ▸ J}{φ₂ : K ▸ L}{φ₃ : M ▸ N}
       where

open import Function renaming (_∘_ to _f∘_)

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Chapter8.Container.Morphism.Contornament

_∙_ : (υ : Contornament φ₁ u₂₁ v₂₁) → 
      Contornament (⟦ υ ⟧corn) u₃₂ v₃₂ → 
      Contornament φ₁ (u₂₁ f∘ u₃₂) (v₂₁ f∘ v₃₂)
υ ∙ τ = 
  record { extend = λ n sh₁ → Σ[ e₁ ∈ extend υ (v₃₂ n) sh₁ ]  extend τ n (sh₁ , e₁)
         ; refine = λ { {n}{sh₁} (e₁ , e₂) p₁ → refine τ e₂ p₁ }
         ; coherence⊢ = λ { {n} sh (e₁ , e₂) p₁ → 
                            trans (cong u₂₁ (coherence⊢ τ (sh , e₁) e₂ p₁)) 
                                  (coherence⊢ υ sh e₁ p₁) } }
  where open Contornament