How to use lifts?

Stream: new members

[Fernando Chu]

Hi, I'm trying to formalize that the grothendieck construction is prefibered, but I'm unsure how to prove the sorry in the base below, as a'.base should be equal to b; but I don't know how to obtain this from the data in the context.

import Mathlib.CategoryTheory.Bicategory.Grothendieck
import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
import Mathlib.CategoryTheory.FiberedCategory.Fibered

open CategoryTheory Functor Category Opposite Discrete Bicategory Pseudofunctor.Grothendieck

universe w v₁ v₂ v₃ u₁ u₂ u₃
variable {𝒮 : Type u₁} [Category.{v₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat.{v₂, u₂}}

instance isPreFibered : IsPreFibered (forget F) := by
  constructor; intro a b f
  exact
    ⟨ { base := b, fiber := (F.map f.op.toLoc).obj a.fiber } ,
      { base := f , fiber := 𝟙 _ } ,
      { universal_property := by
          intro a' g
          exact ⟨ { base := sorry , fiber := sorry } , sorry⟩
        cond := sorry } ⟩

Any help on this, or feedback is appreciated.

[Johan Commelin]

Here's how I filled in the first sorry. Note that I added hfg to the intro line.
The have demonstrates one way to use it.

instance isPreFibered : IsPreFibered (forget F) := by
  constructor; intro a b f
  exact
    ⟨ { base := b, fiber := (F.map f.op.toLoc).obj a.fiber } ,
      { base := f , fiber := 𝟙 _ } ,
      { universal_property := by
          rintro a' g hfg
          have := IsHomLift.fac (forget F) f g
          exact ⟨ { base := eqToHom <| IsHomLift.domain_eq (forget F) f g, fiber := sorry } , sorry⟩
        cond := sorry } ⟩

[Fernando Chu]

Great, thank you!