open import Chapter5.Container

module Chapter8.Container.Morphism.Contornament.Composition.Horizontal
         {I J K L I' J' K' L' : Set}
         {u₁ : I' → I}{v : J' → J}{v₂ : K' → K}
         {φ₁ : I ▸ J}{φ₂ : J ▸ K}
       where

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

open import Data.Product

open import Relation.Binary.PropositionalEquality hiding (subst₂)

open import Chapter2.Equality

open import Chapter5.Container.Composition renaming (_∘_ to _c∘_)

open import Chapter8.Container.Morphism.Contornament


_∘_ : Contornament φ₂ v v₂ → 
      Contornament φ₁ u₁ v  →
      Contornament (φ₂ c∘ φ₁) u₁ v₂
υ ∘ τ = 
  record { extend = extend∘
         ; refine = λ {k'}{sh} → refine∘ {k'}{sh}
         ; coherence⊢ = λ {k'} → coherence∘⊢ {k'} }
  where open Contornament
  
        extend∘ : (k' : K') → S (φ₂ c∘ φ₁) (v₂ k') → Set
        extend∘ k' (sh₂ , pos₂)  =
          Σ[ e₂ ∈ extend υ k' sh₂ ]
           ((p₂ : P φ₂ sh₂) →
                 extend τ _ (subst (S φ₁) 
                            (sym (coherence⊢ υ sh₂ e₂ p₂)) 
                            (pos₂ p₂)))

        refine∘ : {k' : K'}{sh : S (φ₂ c∘ φ₁) (v₂ k')} → 
                  (e : extend∘ k' sh) → P (φ₂ c∘ φ₁) sh → I'
        refine∘ {k'} {sh₂ , pos₂} (e₁ , e₂) (p₂ , p₁) = 
          refine τ (e₂ p₂) 
                 (subst₂ (λ i sh → P φ₁ {i} sh)
                         (sym (coherence⊢ υ sh₂ e₁ p₂)) p₁)

        coherence∘⊢ : {k' : K'}
                     (sh : S (φ₂ c∘ φ₁) (v₂ k'))
                     (e : extend∘ k' sh)
                     (p : P (φ₂ c∘ φ₁) sh) →
                     u₁ (refine∘ e p) ≡ n φ₁ (proj₂ p)
        coherence∘⊢ (sh₂ , pos₂) (e₂ , e₁) (p₂ , p₁) = 
          trans q (sym (cong₃ (λ i sh → n φ₁ {i}{sh}) 
                       (sym (coherence⊢ υ sh₂  e₂ p₂))))

          where q : u₁ (refine τ (e₁ p₂) ((subst₂ (λ i → P φ₁ {i} ) 
                                         (sym (coherence⊢ υ sh₂ e₂ p₂)) 
                                         p₁))) ≡ n φ₁ (subst₂ (λ i → P φ₁ {i} ) 
                                         (sym (coherence⊢ υ sh₂ e₂ p₂)) 
                                         p₁)
                q = coherence⊢ τ (subst (S φ₁) 
                                        (sym (coherence⊢ υ sh₂ e₂ p₂)) 
                                        (pos₂ p₂)) 
                                 (e₁ p₂) 
                                 (subst₂ (λ i → P φ₁ {i} ) 
                                         (sym (coherence⊢ υ sh₂ e₂ p₂)) 
                                         p₁)