Zulip Chat Archive

Stream: Is there code for X?

Topic: functor.comp as a functor


view this post on Zulip Adam Topaz (Mar 03 2021 at 21:04):

Do we have the following two sorry's in mathlib somewhere?

import category_theory.equivalence

namespace category_theory

variables {B C D : Type*} [category B] [category C] [category D]

def foo (F : C  D) : (B  C)  (B  D) := sorry

def bar (F : C  D) : (B  C)  (B  D) := sorry

end category_theory

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:06):

Okay, I found the second one: docs#category_theory.equivalence.congr_right

view this post on Zulip Adam Topaz (Mar 03 2021 at 21:06):

Ah, and the first is just docs#category_theory.whiskering_right


Last updated: May 07 2021 at 19:12 UTC