mathlib documentation

category_theory.category.ulift

Basic API for ulift #

This file contains a very basic API for working with the categorical instance on ulift C where C is a type with a category instance.

  1. category_theory.ulift.up is the functorial version of the usual ulift.up.
  2. category_theory.ulift.down is the functorial version of the usual ulift.down.
  3. category_theory.ulift.equivalence is the categorical equivalence between C and ulift C.
@[simp]
theorem category_theory.ulift.up_map {C : Type u1} [category_theory.category C] (X Y : C) (f : X Y) :

The functorial version of ulift.up.

Equations
@[simp]

The functorial version of ulift.down.

Equations
@[simp]