case H
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ ↑(mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = ↑(Equiv.refl (F α α')) x
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
ext x
no goals
case H
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ ↑(mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = ↑(Equiv.refl (F α α')) x
simp [id_bimap]