Zulip Chat Archive

Stream: Copenhagen Masterclass 2023

Topic: Effective empimorphism stuff

Jon Eugster (Jun 26 2023 at 11:15):

I'd like to join!

Sina (Jun 26 2023 at 11:15):

interested.

Jon Eugster (Jun 26 2023 at 11:44):

set_option trace.Meta.synthInstance true in to see instance

Boris Kjær (Jun 26 2023 at 11:47):

Move topic to https://leanprover.zulipchat.com/#narrow/stream/384459-Copenhagen-Masterclass-2023/topic/TFAE.20fam.20of.20epis

Boris Kjær (Jun 26 2023 at 12:06):

CompHaus proofs lake-packages/mathlib/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Last updated: Dec 20 2023 at 11:08 UTC