{-# OPTIONS --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Transport

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Displayed.Base

module Cubical.Categories.Displayed.Reasoning
  {ℓC ℓ'C ℓCᴰ ℓ'Cᴰ : Level}
  {C : Category ℓC ℓ'C}
  (Cᴰ : Categoryᴰ C ℓCᴰ ℓ'Cᴰ)
  where

  open Categoryᴰ Cᴰ
  private module C = Category C
  open Category hiding (_∘_)

  reind : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
    → Hom[ f ][ aᴰ , bᴰ ] → Hom[ g ][ aᴰ , bᴰ ]
  reind p = subst Hom[_][ _ , _ ] p

  reind-filler : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      (f : Hom[ f ][ aᴰ , bᴰ ])
    → f ≡[ p ] reind p f
  reind-filler p = subst-filler Hom[_][ _ , _ ] p

  reind-filler-sym : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      (f : Hom[ g ][ aᴰ , bᴰ ])
    → reind (sym p) f ≡[ p ] f
  reind-filler-sym p = symP ∘ reind-filler (sym p)

  ≡[]-rectify : {a b : C.ob} {f g : C [ a , b ]} {p p' : f ≡ g}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
    → fᴰ ≡[ p ] gᴰ → fᴰ ≡[ p' ] gᴰ
  ≡[]-rectify {fᴰ = fᴰ} {gᴰ = gᴰ} = subst (fᴰ ≡[_] gᴰ) (C.isSetHom _ _ _ _)

  ≡[]∙ : {a b : C.ob} {f g h : C [ a , b ]}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
      {hᴰ : Hom[ h ][ aᴰ , bᴰ ]}
      (p : f ≡ g) (q : g ≡ h)
    → fᴰ ≡[ p ] gᴰ
    → gᴰ ≡[ q ] hᴰ → fᴰ ≡[ p ∙ q ] hᴰ
  ≡[]∙ {fᴰ = fᴰ} {hᴰ = hᴰ} p q eq1 eq2 =
    subst
      (λ p → PathP (λ i → p i) fᴰ hᴰ)
      (sym $ congFunct Hom[_][ _ , _ ] p q)
      (compPathP eq1 eq2)

  infixr  ≡[]∙
  syntax ≡[]∙ p q eq1 eq2 = eq1 [ p ]∙[ q ] eq2

  ≡[]⋆ : {a b c : C.ob} {f g : C [ a , b ]} {h i : C [ b , c ]}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
      {hᴰ : Hom[ h ][ bᴰ , cᴰ ]}
      {iᴰ : Hom[ i ][ bᴰ , cᴰ ]}
      (p : f ≡ g) (q : h ≡ i)
    → fᴰ ≡[ p ] gᴰ → hᴰ ≡[ q ] iᴰ → fᴰ ⋆ᴰ hᴰ ≡[ cong₂ C._⋆_ p q ] gᴰ ⋆ᴰ iᴰ
  ≡[]⋆ _ _ = congP₂ (λ _ → _⋆ᴰ_)

  infixr  ≡[]⋆
  syntax ≡[]⋆ p q eq1 eq2 = eq1 [ p ]⋆[ q ] eq2

  reind-rectify : {a b : C.ob} {f g : C [ a , b ]} {p p' : f ≡ g}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
    → reind p fᴰ ≡ reind p' fᴰ
  reind-rectify {fᴰ = fᴰ} = cong (λ p → reind p fᴰ) (C.isSetHom _ _ _ _)

  reind-contractʳ : {a b c : C.ob} {f g : C [ a , b ]} {h : C [ b , c ]}
      {p : f ≡ g}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]} {hᴰ : Hom[ h ][ bᴰ , cᴰ ]}
    → reind (cong (C._⋆ h) p) (fᴰ ⋆ᴰ hᴰ) ≡ reind p fᴰ ⋆ᴰ hᴰ
  reind-contractʳ {hᴰ = hᴰ} = fromPathP $
    congP (λ _ → _⋆ᴰ hᴰ) (transport-filler _ _)

  reind-comp : {a b : C.ob} {f g h : C [ a , b ]} {p : f ≡ g} {q : g ≡ h}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
    → reind (p ∙ q) fᴰ ≡ reind q (reind p fᴰ)
  reind-comp = substComposite Hom[_][ _ , _ ] _ _ _

  reind-contractˡ : {a b c : C.ob} {f : C [ a , b ]} {g h : C [ b , c ]}
      {p : g ≡ h}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]} {gᴰ : Hom[ g ][ bᴰ , cᴰ ]}
    → reind (cong (f C.⋆_) p) (fᴰ ⋆ᴰ gᴰ) ≡ fᴰ ⋆ᴰ reind p gᴰ
  reind-contractˡ {fᴰ = fᴰ} = fromPathP $
    congP (λ _ → fᴰ ⋆ᴰ_) (transport-filler _ _)

  ≡→≡[] : {a b : C.ob} {f g : C [ a , b ]} {p : f ≡ g}
      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
    → reind p fᴰ ≡ gᴰ → fᴰ ≡[ p ] gᴰ
  ≡→≡[] = toPathP