open import Chapter5.Container open import Chapter5.Container.Composition renaming (_∘_ to _c∘_) open import Chapter8.Container.Morphism.Contornament module Chapter8.Container.Morphism.Contornament.Pullback {K₁ L₁ K₂ L₂ I J : Set} {u₁ : K₁ → I}{v₁ : L₁ → J} {u₂ : K₂ → I}{v₂ : L₂ → J} {φ : I ▸ J} where open import Function renaming (_∘_ to _f∘_) open import Data.Product open import Relation.Binary.PropositionalEquality hiding (subst₂) open import Chapter2.Equality _×_[_∶_] : (K₁ : Set){I : Set}(K₂ : Set)(u₁ : K₁ → I)(u₂ : K₂ → I) → Set K₁ × K₂ [ u₁ ∶ u₂ ] = Σ[ k₁ ∈ K₁ ] Σ[ k₂ ∈ K₂ ] Σ[ i ∈ _ ] i ≡ u₁ k₁ × i ≡ u₂ k₂ u : K₁ × K₂ [ u₁ ∶ u₂ ] → I u (_ , _ , i , _ , _) = i v : L₁ × L₂ [ v₁ ∶ v₂ ] → J v (_ , _ , j , _ , _) = j _×p_ : Contornament φ u₁ v₁ → Contornament φ u₂ v₂ → Contornament φ u v υ ×p τ = record { extend = extendp ; refine = λ {l}{sh} → refinep {l}{sh} ; coherence⊢ = λ {l} → coherencep {l} } where open Contornament extendp : (l : L₁ × L₂ [ v₁ ∶ v₂ ]) → S φ (v l) → Set extendp (l₁ , l₂ , i , q₁ , q₂) sh = extend υ l₁ (subst (S φ) q₁ sh) × extend τ l₂ (subst (S φ) q₂ sh) refinep : {l : L₁ × L₂ [ v₁ ∶ v₂ ]} {sh : S φ (v l)} → extendp l sh → P φ sh → K₁ × K₂ [ u₁ ∶ u₂ ] refinep {l₁ , l₂ , i , q₁ , q₂}{sh} (e₁ , e₂) p = refine υ {sh = subst (S φ) q₁ sh} e₁ (subst₂ (λ j sh → P φ {j} sh) q₁ p) , refine τ {sh = subst (S φ) q₂ sh} e₂ (subst₂ (λ j sh → P φ {j} sh) q₂ p) , n φ {i} {sh} p , let q = coherence⊢ υ (subst (λ sh → S φ sh) q₁ sh) e₁ (subst₂ (λ i → P φ {i}) q₁ p) in trans (cong₃ (λ i sh → n φ {i}{sh}) q₁) (sym q) , let q = coherence⊢ τ (subst (λ sh → S φ sh) q₂ sh) e₂ (subst₂ (λ i → P φ {i}) q₂ p) in trans (cong₃ (λ i sh → n φ {i}{sh}) q₂) (sym q) coherencep : {l : L₁ × L₂ [ v₁ ∶ v₂ ]} (sh : S φ (v l)) → (e : extendp l sh) (p : P φ sh) → n φ p ≡ u (refinep {l} {sh} e p) coherencep sh e p = refl