-- A natural transformation is *Cartesian* when its naturality squares
-- are pullbacks

module Cubical.Categories.NaturalTransformation.Cartesian where

open import Cubical.Data.Sigma
open import Cubical.Categories.Category renaming (isIso to isIsoC)
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Categories.Limits.Pullback


private
  variable
    ℓA ℓA' ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
    ℓ ℓ' ℓ'' : Level
    B C D E : Category ℓ ℓ'

open Category
open NatTrans
open NatIso
open isIsoC

module _
  {C : Category ℓC ℓC'}
  {D : Category ℓD ℓD'}
  where
  module _ {F G : Functor C D} (α : NatTrans F G) where
    isCartesian : Type _
    isCartesian = ∀ {x y}(f : C [ x , y ])
      → isPullback D (cospan (F ⟅ y ⟆) (G ⟅ y ⟆) (G ⟅ x ⟆) (α ⟦ y ⟧) (G ⟪ f ⟫)) {F ⟅ x ⟆}
          (F ⟪ f ⟫)
          (α ⟦ x ⟧)
          (α .N-hom f)
  CartesianNatTrans : (F G : Functor C D) → Type _
  CartesianNatTrans F G = Σ (NatTrans F G) isCartesian

  module _ {F G : Functor C D} ((α , α-cart) : CartesianNatTrans F G)  where
    CartesianNatTrans→PBSq : ∀ {x y} (f : C [ x , y ]) → Pullback D (cospan (F ⟅ y ⟆) (G ⟅ y ⟆) (G ⟅ x ⟆) (α ⟦ y ⟧) (G ⟪ f ⟫))
    CartesianNatTrans→PBSq {x}{y} f = record
                              { pbOb = F ⟅ x ⟆
                              ; pbPr₁ = F ⟪ f ⟫
                              ; pbPr₂ = α ⟦ x ⟧
                              ; pbCommutes = α .N-hom f
                              ; univProp = α-cart f
                              }
    module CartNatTransPBs {x y} (f : C [ x , y ]) = Pullback (CartesianNatTrans→PBSq f)

module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C C}{F' : Functor D D}
  (G : Functor C D)
  ((π , π-Cart) : CartesianNatTrans F Id)
  ((π' , π'-Cart) : CartesianNatTrans F' Id)
  where
  private
    module D = Category D using (_⋆_)
  preservesCartNatTrans : Type _
  preservesCartNatTrans = Σ[ swap ∈ NatIso (G ∘F F) (F' ∘F G) ]
    (∀ Γ → (swap .trans ⟦ Γ ⟧ D.⋆ π' ⟦ G ⟅ Γ ⟆ ⟧) ≡ G ⟪ π ⟦ Γ ⟧ ⟫)