Free categories

[barrettj12]

I've tried to define the free category over a directed graph. This should make it much easier to define many finite categories (see Categories.Instances.Cospan for what we currently have to do to define the free category over ● → ● ← ●).

I defined a notion of path in a graph to serve as the homset. The issue I'm having is proving that Path v w is a set. I'm guessing it should be true when Node G and Edge G are both sets, but don't see a good way to prove this. One idea I had was to convert paths to lists, then use isOfHLevelRetract and the fact that isSet A → isSet (List A). However, this path-to-list function doesn't have an inverse (for some lists).

Ideas and contributions appreciated.

[mortberg]

If Node and Edge are both sets then it should be a set. Unless I'm confused this is Lemma 4.2 in https://arxiv.org/abs/2112.06609

[barrettj12]

If Node and Edge are both sets then it should be a set. Unless I'm confused this is Lemma 4.2 in https://arxiv.org/abs/2112.06609

Thanks, good catch. I've tried to formalise this but I'm running into universe levels. The --cumulativity flag fixed that, but now Agda can't solve the level constraints.

[mortberg]

If Node and Edge are both sets then it should be a set. Unless I'm confused this is Lemma 4.2 in https://arxiv.org/abs/2112.06609

Thanks, good catch. I've tried to formalise this but I'm running into universe levels. The --cumulativity flag fixed that, but now Agda can't solve the level constraints.

Hmm, can you get it to work if everything is at the same level (so not separate levels for nodes and edges)? Might be a good start. Most (all?) examples used for defining (co)limits should have the nodes and graphs in level 0 anyway

[barrettj12]

@mortberg I've now completed this for the case where nodes and edges have the same universe levels.

I still get a problem with the definition of PathWithLen in the general case, since v ≡ w : Type ℓv, not Type (ℓ-max ℓv ℓe). I can fix this using the --cumulativity flag, but then other nasty unification issues and other Agda errors pop up.

However, I was wondering if it could be fixed by defining something like

data tlift (A : Type ℓv) : Type (ℓ-max ℓv ℓe) where
  ↑↑ : A → tlift A

and then using tlift (v ≡ w) instead of v ≡ w. Is something like tlift defined anywhere in the library?

[mortberg]

How does one get the CI to run for this PR?

[barrettj12]

@mortberg from memory, the code doesn't type check yet - see my comment dated 29 Dec 2021.

[ecavallo]

Is something like tlift defined anywhere in the library?

Yes, there is a type called Lift defined in Foundations.Prelude.