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