cone equiv

Stream: Is there code for X?

[Adam Topaz]

I'm sure we have some way of formulating the following, but I can't seem to find it...

import category_theory.limits.cones

open category_theory
open category_theory.limits

universe v
variables {J : Type v} {C : Type*} [category.{v} C] [small_category J] {F G : J ⥤ C} (η : F ≅ G)

def foobar : cone F ≃ cone G :=
{ to_fun := λ E, ⟨E.X, E.π ≫ η.hom⟩,
  inv_fun := λ E, ⟨E.X, E.π ≫ η.inv⟩,
  left_inv := by { rintros ⟨X,E⟩, simp },
  right_inv := by { rintros ⟨X,E⟩, simp } }

[Adam Topaz]

Ah ok, it's docs#category_theory.limits.cones.postcompose_equivalence

[Adam Topaz]

What about this?

import category_theory.limits.cones
import category_theory.limits.is_limit

open category_theory
open category_theory.limits

universe v
variables {J : Type v} {C : Type*} [category.{v} C] [small_category J] {F G : J ⥤ C} (η : F ≅ G)

def foobar (E : cone F) (hE : is_limit E) : is_limit ((cones.postcompose η.hom).obj E) :=
{ lift := λ S, hE.lift ((cones.postcompose η.inv).obj S),
  fac' := sorry,
  uniq' := sorry }

[Adam Topaz]

ping @Bhavik Mehta

[Bhavik Mehta]

I'm pretty sure it's in is_limit somewhere, let me find it for you

[Bhavik Mehta]

It's the reverse direction of docs#is_limit.postcompose_hom_equiv

[Adam Topaz]

Thanks!