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