free or walking isomorphism?

Stream: Is there code for X?

[Emily Riehl]

Does mathlib know about the free category containing an isomorphism, which has two objects and a unique arrow in each hom-set? The quiver structure could be defined as follows:

/-- This is the free-living isomorphism as a category with objects called
`zero` and `one`. Perhaps these should have different names like `src` and `tgt`?-/
inductive walkingIso : Type u where
  | zero : walkingIso
  | one : walkingIso

open walkingIso

namespace WalkingIso

/-- The arrows in the walking iso category split into three cases.-/
inductive Hom : walkingIso → walkingIso → Type v where
  | id : (X : walkingIso) → Hom X X
  | hom : Hom zero one
  | inv : Hom one zero

/-- The quiver structure on `walkingIso`-/
instance : Quiver walkingIso where
  Hom := Hom

end WalkingIso

[Adam Topaz]

I don't think we have this.

[Kim Morrison]

What does this definition gain over just Hom X Y := PUnit?

[Emily Riehl]

I had thought it might be better to give explicit names for the key arrows? But then we ended up writing inductive proofs that were annoying and unenlightening. You and @Joël Riou have convinced me that using PUnit is better.

[Emily Riehl]

Relatedly, it seems that mathlib doesn't have a notion of "indiscrete" or "chaotic" or "contractible" category, defining the right adjoint to the functor ob : Cat -> Set. While "discrete" categories already exist, it seems that they haven't been shown to define the left adjoint to this functor either.

I have some students looking for a beginner category theory project, so I might suggest this to them. Which name do folks prefer?

[Johan Commelin]

I'll vote for Indiscrete

[Dagur Asgeirsson]

Emily Riehl said:

While "discrete" categories already exist, it seems that they haven't been shown to define the left adjoint to this functor either.

I'm pretty sure this is in mathlib, let me find it

[Dagur Asgeirsson]

docs#CategoryTheory.Cat.typeToCatObjectsAdj

[Dagur Asgeirsson]

But indeed we do not have the right adjoint

[Kim Morrison]

I like Indiscrete too, or Contractible just as much.