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