C : Type u
inst✝ : Category C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
⊢ HasColimitsOfShape J C
C : Type u
inst✝ : Category C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape J C
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
C : Type u
inst✝ : Category C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasColimitsOfShape J C
C : Type u
inst✝ : Category C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
⊢ HasColimitsOfShape J C
have l :
  @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ))
  := @ULiftHomULiftCategory.equiv J hJ
no goals
C : Type u
inst✝ : Category C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasColimitsOfShape J C
apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
  (@Equivalence.symm J hJ (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _