open import Cat.Functor.Equivalence
open import Cat.Instances.Functor
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

module
  wip.test2
    {o ℓ o′ ℓ′ o′′ ℓ′′} 
    {X : Precategory o ℓ} {B : Precategory o′ ℓ′} 
    (F : Functor X B)
    (E : Displayed B o′′ ℓ′′)
  where

module E = Displayed E
module X = Precategory X
module B = Precategory B
open Displayed
open Functor F

subst-hom : ∀ {a b x y} {f g : B.Hom a b} → f ≡ g → E.Hom[ f ] x y → E.Hom[ g ] x y
subst-hom p f′ = subst (λ h → E.Hom[ h ] _ _) p f′

subst-hom-∙ : ∀ {a b x y} {f g h : B.Hom a b} (p : f ≡ g) (q : g ≡ h) 
                {f′ : E.Hom[ f ] x y}
            → subst-hom q (subst-hom p f′) ≡ subst-hom (p ∙ q) f′
subst-hom-∙ p q = sym (subst-∙ (λ h → E.Hom[ h ] _ _) _ _ _)

subst-hom-whiskerʳ : ∀ {a b c} {f : B.Hom b c} {g g' : B.Hom a b} {a′ b′ c′} 
                       {f′ : E.Hom[ f ] b′ c′}
                       {g′ : E.Hom[ g ] a′ b′}
                       (p : g ≡ g')
                   → f′ E.∘′ subst-hom p g′ ≡ subst-hom (ap (f B.∘_) p) (f′ E.∘′ g′)
subst-hom-whiskerʳ {f = f} {g} {g'} {a′} {b′} {c′} {f′} {g′} p i = 
  comp (λ j → E.Hom[ f B.∘ p (i ∨ j) ] a′ c′) 
    (λ { j (i = i0) → f′ E.∘′ transport-filler (λ i → E.Hom[ p i ] _ _) g′ j
       ; j (i = i1) → subst-hom (ap (f B.∘_) p) (f′ E.∘′ g′)
       }) 
    (transport-filler (λ i → E.Hom[ f B.∘ p i ] _ _) (f′ E.∘′ g′) i)
  -- ^ this is a super cursed square. super cursed. it's infinitely
  -- better behaved than it was with J, though

subst-hom-whiskerˡ : ∀ {a b c} {f f' : B.Hom b c} {g : B.Hom a b} {a′ b′ c′} 
                       {f′ : E.Hom[ f ] b′ c′}
                       {g′ : E.Hom[ g ] a′ b′}
                       (p : f ≡ f')
                   → subst-hom p f′ E.∘′ g′ ≡ subst-hom (ap (B._∘ g) p) (f′ E.∘′ g′)
subst-hom-whiskerˡ {f = f} {f'} {g} {a′} {b′} {c′} {f′} {g′} p i =
  comp (λ j → E.Hom[ p (i ∨ j) B.∘ g ] a′ c′) 
    (λ { j (i = i0) → transport-filler (λ i → E.Hom[ p i ] _ _) f′ j E.∘′ g′
       ; j (i = i1) → subst-hom (ap (B._∘ g) p) (f′ E.∘′ g′)
       }) 
    (transport-filler (λ i → E.Hom[ p i B.∘ g ] _ _) (f′ E.∘′ g′) i)

Change-of-base : Displayed X o′′ ℓ′′
Change-of-base .Ob[_] x = E.Ob[ F₀ x ]
Change-of-base .Hom[_] f x y = E.Hom[ F₁ f ] x y
Change-of-base .Hom[_]-set f = E.Hom[ F₁ f ]-set
Change-of-base .id′ = subst-hom (sym F-id) E.id′
Change-of-base ._∘′_ f′ g′ = subst-hom (sym (F-∘ _ _)) (f′ E.∘′ g′)
Change-of-base .idr′ f′ = 
  to-pathp (
       subst-hom-∙ _ _ 
    ·· ap (subst-hom _) (subst-hom-whiskerʳ _) 
    ·· subst-hom-∙ _ _ 
    ·· ap (λ e → subst-hom e (f′ E.∘′ E.id′)) (B.Hom-set _ _ _ _ _ _) 
    ·· from-pathp (E.idr′ f′))

Change-of-base .idl′ f′ = 
  to-pathp (
       subst-hom-∙ _ _ 
    ·· ap (subst-hom _) (subst-hom-whiskerˡ _) 
    ·· subst-hom-∙ _ _ 
    ·· ap (λ e → subst-hom e (E.id′ E.∘′ f′)) (B.Hom-set _ _ _ _ _ _) 
    ·· from-pathp (E.idl′ f′))

Change-of-base .assoc′ f′ g′ h′ =
  to-pathp (
       subst-hom-∙ _ _ 
    ·· ap (subst-hom _) (subst-hom-whiskerʳ _) 
    ·· subst-hom-∙ _ _
    ·· ap (λ e → subst-hom e (f′ E.∘′ g′ E.∘′ h′)) 
            (B.Hom-set _ _ _ _ _ ( B.assoc _ _ _ 
                                 ∙ ap (B._∘ _) (sym (F-∘ _ _)) 
                                 ∙ sym (F-∘ _ _)))
    ·· sym (subst-hom-∙ _ _)
    ·· ap (subst-hom _) (from-pathp (E.assoc′ f′ g′ h′)) 
    ·· sym (ap (subst-hom _) (subst-hom-whiskerˡ _) ∙ subst-hom-∙ _ _))