## Stream: maths

### Topic: connected categories

#### Reid Barton (Sep 12 2018 at 16:57):

I took a stab at defining an "interface" for what it means for a category to be connected and used it to prove a standard fact about cofinal functors. @Mario Carneiro I'm curious to hear whether you would suggest any improvements.
https://gist.github.com/rwbarton/1ce6aabec33d47213ed11c5b7d907a4f

#### Reid Barton (Sep 12 2018 at 16:59):

I didn't bother actually defining connected as I figure it's easy once you have the interface right. So the interface is the three axioms. components is not used directly, but the definition of connected should make proving connected_iff_components_trivial easy so it should probably be related to components in some way.

#### Reid Barton (Sep 12 2018 at 17:05):

I guess I didn't include any way to prove that a category is connected, but I feel like that side of things should be easier

#### Reid Barton (Sep 12 2018 at 17:43):

Actually I need the inv_fun direction of connected_iff_components_trivial elsewhere, so that can also be considered part of the interface

Last updated: May 06 2021 at 17:38 UTC