open import Chapter5.Container

open import Chapter8.Container.Morphism.Cartesian

module Chapter8.Container.Morphism.Cartesian.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 Relation.Binary.PropositionalEquality


_•_ : φ₂ ⇒c[ u₂₁  v₂₁ ] φ₁  φ₃ ⇒c[ u₃₂  v₃₂ ] φ₂  
      φ₃ ⇒c[ u₂₁ f∘ u₃₂  v₂₁ f∘ v₃₂ ] φ₁
τ₁  τ₂ = record { σ = λ sh  σ τ₁ (σ τ₂ sh)
           ; ρ = trans (ρ τ₁) (ρ τ₂)
           ; q = λ p  trans 
                         (cong u₂₁ 
                           (trans 
                             (cong  p  u₃₂ (n φ₃ p))
                                   (pf (ρ τ₂) (ρ τ₁) p)) 
                             (q τ₂ (subst id (ρ τ₁) p)))) 
                         (q τ₁ p) }
    where open _⇒c[_∣_]_ public

          pf : ∀{A B C : Set}  (q₂ : B  C)(q₁ : A  B)(p : A) 
                   subst id (trans q₁ q₂) p  subst id q₂ (subst id q₁ p)
          pf refl refl p = refl