# Zulip Chat Archive

## Stream: new members

### Topic: can't find instance

#### Rémi Bottinelli (Oct 15 2022 at 13:29):

Hi, I'm trying to refactor the `quiver`

code a bit and got into some instance troubles.

here, lean doesn't find the necessary `quiver`

instance on `V`

, even though I have an instance as a variable.

I'm pretty sure it's related to universe incompatibilities, but can't really figure out where they come from.

I can't really get a MWE out of that: what kind of approach should I take to debug this?

#### Yaël Dillies (Oct 15 2022 at 13:37):

Try `set_option pp.universes true`

#### Rémi Bottinelli (Oct 15 2022 at 13:39):

OK, I get

```
failed to synthesize type class instance for
V : Type u,
_inst_1 : quiver.{u_1 u} V,
H : wide_subquiver.{u ?l_1} (symmetrify.{u} V)
⊢ quiver.{?l_2+1 u} V
```

which I guess is related to the transition to `psum`

, maybe?

#### Yaël Dillies (Oct 15 2022 at 13:39):

Yeah, very possible...

#### Rémi Bottinelli (Oct 15 2022 at 13:45):

Alright… I'm a bit clueless as to how to fix that so I might leave that aside for a while. Thanks!

#### Eric Wieser (Oct 15 2022 at 13:49):

This feels like a `Type`

vs `Sort`

issue

#### Rémi Bottinelli (Oct 15 2022 at 13:59):

Indeed, but no idea what's the cause

#### Eric Wieser (Oct 15 2022 at 14:02):

Do things become more obvious if you use `[quiver.{v} V]`

for a new universe `v`

?

#### Eric Wieser (Oct 15 2022 at 14:05):

I would guess that `quiver.{v+1} V`

solves the issue

#### Rémi Bottinelli (Oct 15 2022 at 14:05):

let me see

#### Rémi Bottinelli (Oct 15 2022 at 14:05):

lol, it does…

#### Rémi Bottinelli (Oct 15 2022 at 14:06):

But am I risking a kind of domino effect here where the `+1`

has to be appended everytime?

#### Eric Wieser (Oct 15 2022 at 14:10):

I expect the real solution is to change a `Type`

to a `Sort`

somewhere

#### Rémi Bottinelli (Oct 15 2022 at 14:14):

One of the thing I did was change `symmetrify`

from being defined as `sum (x --> y) (y --> X)`

to `psum …`

, so that I can symmetrify a `Prop`

ositional quiver. This could mean that this is simply incompatible with doing things cleanly?

#### Eric Wieser (Oct 15 2022 at 14:19):

Does `V : Sort*`

work?

#### Rémi Bottinelli (Oct 15 2022 at 14:22):

quivers take `V : Type*`

, so doing that would imply redefining quivers themselves, no?

#### Rémi Bottinelli (Oct 15 2022 at 14:22):

I'm trying, but it's not entirely mechanical afaict

#### Rémi Bottinelli (Oct 15 2022 at 14:23):

(and redefining quivers would redefine categories I guess… which looks quite dangerous to me)

#### Eric Wieser (Oct 15 2022 at 14:23):

Do they? docs#quiver

#### Yaël Dillies (Oct 15 2022 at 14:24):

Yes, there's a difference between the index type and the return type of the homs.

#### Eric Wieser (Oct 15 2022 at 14:24):

Yes. Then my `Sort`

suggestion is a bad idea!

#### Rémi Bottinelli (Oct 15 2022 at 14:24):

(haha I'm relieved I don't have to go there :) )

#### Eric Wieser (Oct 15 2022 at 14:26):

Maybe docs#wide_subquiver is the issue?

#### Rémi Bottinelli (Oct 15 2022 at 14:32):

Mmh, that would make sense, and then I'd only have to "up" the level there, but I actually get other errors somewhere else also related to bad universes.

To be more precise: now it's `category_theory/groupoid/free_groupoid.lean`

that complains: the abbreviations at the beginning fail already.

#### Rémi Bottinelli (Oct 15 2022 at 14:34):

Doesn't `set`

support `Prop`

types?

#### Rémi Bottinelli (Oct 15 2022 at 14:39):

Bargh, got to go, thanks for the help debugging this!

#### Kevin Buzzard (Oct 15 2022 at 14:49):

Scott Morrison once tried to generalise the category theory library so that it allowed morphisms to take values in Sort u rather than Type u and after some struggling he gave up on the idea and reverted. This feels like the same sort of thing

#### Yaël Dillies (Oct 15 2022 at 14:51):

... which is really a shame, because that would allow us to unify orders and categories.

#### Rémi Bottinelli (Oct 15 2022 at 15:54):

mmh, that's sad indeed

#### Rémi Bottinelli (Dec 12 2022 at 07:45):

The `symmetrify`

code has been ported to mathlib4, and it seems the universe problem disappears, so that one should be able to take `symmetrify V`

as a `PSum`

rather than a `Sum`

. Is making such a change incompatible with the port having to be kind of 1-1 ?

```
/-
Copyright (c) 2021 David Wärn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Wärn
Ported by: Joël Riou
-/
import Mathlib.Combinatorics.Quiver.Subquiver
import Mathlib.Combinatorics.Quiver.Path
import Mathlib.Data.Sum.Basic
/-!
## Weakly connected components
For a quiver `V`, we build a quiver `Symmetrify V` by adding a reversal of every edge.
Informally, a path in `Symmetrify V` corresponds to a 'zigzag' in `V`. This lets us
define the type `WeaklyConnectedComponent V` as the quotient of `V` by the relation which
identifies `a` with `b` if there is a path from `a` to `b` in `Symmetrify V`. (These
zigzags can be seen as a proof-relevant analogue of `EqvGen`.)
Strongly connected components have not yet been defined.
-/
universe v u
namespace Quiver
/-- A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow).
NB: this does not work for `Prop`-valued quivers. It requires `[Quiver.{v+1} V]`. -/
-- Porting note: no hasNonemptyInstnace linter yet
def Symmetrify (V : Type u) :=
V
instance symmetrifyQuiver (V : Type u) [Quiver V] : Quiver (Symmetrify V) :=
⟨fun a b : V ↦ PSum (a ⟶ b) (b ⟶ a)⟩
variable (V : Type u) [Quiver V]
/-- A quiver `HasReverse` if we can reverse an arrow `p` from `a` to `b` to get an arrow
`p.reverse` from `b` to `a`.-/
class HasReverse where
/-- the map which sends an arrow to its reverse -/
reverse' : ∀ {a b : V}, (a ⟶ b) → (b ⟶ a)
/-- Reverse the direction of an arrow. -/
def reverse {V} [Quiver V] [HasReverse V] {a b : V} : (a ⟶ b) → (b ⟶ a) :=
HasReverse.reverse'
/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity.`-/
class HasInvolutiveReverse extends HasReverse V where
/-- `reverse` is involutive -/
inv' : ∀ {a b : V} (f : a ⟶ b), reverse (reverse f) = f
@[simp]
theorem reverse_reverse {V} [Quiver V] [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) :
reverse (reverse f) = f := by apply h.inv'
variable {V}
instance : HasReverse (Symmetrify V) :=
⟨fun e ↦ match e with
| (PSum.inl f) => PSum.inr f
| (PSum.inr f) => PSum.inl f⟩
instance :
HasInvolutiveReverse
(Symmetrify V) where
toHasReverse := ⟨fun e ↦
match e with
| (PSum.inl f) => PSum.inr f
| (PSum.inr f) => PSum.inl f⟩
inv' e :=
match e with
| (PSum.inl _) => rfl
| (PSum.inr _) => rfl
/-- Reverse the direction of a path. -/
@[simp]
def Path.reverse [HasReverse V] {a : V} : ∀ {b}, Path a b → Path b a
| _, Path.nil => Path.nil
| _, Path.cons p e => (Quiver.reverse e).toPath.comp p.reverse
@[simp]
theorem Path.reverse_toPath [HasReverse V] {a b : V} (f : a ⟶ b) :
f.toPath.reverse = (Quiver.reverse f).toPath :=
rfl
#align quiver.path.reverse_to_path Quiver.Path.reverse_toPath
@[simp]
theorem Path.reverse_comp [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
(p.comp q).reverse = q.reverse.comp p.reverse := by
induction' q with _ _ _ _ h
· simp
· simp [h]
@[simp]
theorem Path.reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (p : Path a b) :
p.reverse.reverse = p := by
induction' p with _ _ _ _ h
· simp
· rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
rfl
/-- The inclusion of a quiver in its symmetrification -/
def Symmetrify.of : Prefunctor V (Symmetrify V) where
obj := id
map := PSum.inl
/-- Given a quiver `V'` with reversible arrows, a prefunctor to `V'` can be lifted to one from
`Symmetrify V` to `V'` -/
def Symmetrify.lift {V' : Type _} [Quiver V'] [HasReverse V'] (φ : Prefunctor V V') :
Prefunctor (Symmetrify V) V' where
obj := φ.obj
map f := match f with
| PSum.inl g => φ.map g
| PSum.inr g => reverse (φ.map g)
theorem Symmetrify.lift_spec (V' : Type _) [Quiver V'] [HasReverse V'] (φ : Prefunctor V V') :
Symmetrify.of.comp (Symmetrify.lift φ) = φ := by
fapply Prefunctor.ext
· rintro X
rfl
· rintro X Y f
rfl
theorem Symmetrify.lift_reverse (V' : Type _) [Quiver V'] [h : HasInvolutiveReverse V']
(φ : Prefunctor V V') {X Y : Symmetrify V} (f : X ⟶ Y) :
(Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Symmetrify.lift φ).map f) := by
dsimp [Symmetrify.lift]; cases f
· simp only
rfl
· simp only
rw [h.inv']
rfl
/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses. -/
theorem Symmetrify.lift_unique (V' : Type _) [Quiver V'] [HasReverse V'] (φ : Prefunctor V V')
(Φ : Prefunctor (Symmetrify V) V') (hΦ : Symmetrify.of.comp Φ = φ)
(hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) :
Φ = Symmetrify.lift φ := by
subst_vars
fapply Prefunctor.ext
· rintro X
rfl
· rintro X Y f
cases f
· rfl
· exact hΦinv (PSum.inl _)
#align quiver.symmetrify.lift_unique Quiver.Symmetrify.lift_unique
variable (V)
/-- Two vertices are related in the zigzag setoid if there is a
zigzag of arrows from one to the other. -/
def zigzagSetoid : Setoid V :=
⟨fun a b ↦ Nonempty (@Path (Symmetrify V) _ a b), fun _ ↦ ⟨Path.nil⟩, fun ⟨p⟩ ↦
⟨p.reverse⟩, fun ⟨p⟩ ⟨q⟩ ↦ ⟨p.comp q⟩⟩
/-- The type of weakly connected components of a directed graph. Two vertices are
in the same weakly connected component if there is a zigzag of arrows from one
to the other. -/
def WeaklyConnectedComponent : Type u :=
Quotient (zigzagSetoid V)
namespace WeaklyConnectedComponent
variable {V}
/-- The weakly connected component corresponding to a vertex. -/
protected def mk : V → WeaklyConnectedComponent V :=
@Quotient.mk' _ (zigzagSetoid V)
instance : CoeTC V (WeaklyConnectedComponent V) :=
⟨WeaklyConnectedComponent.mk⟩
instance [Inhabited V] : Inhabited (WeaklyConnectedComponent V) :=
⟨show V from default⟩
protected theorem eq (a b : V) :
(a : WeaklyConnectedComponent V) = b ↔ Nonempty (@Path (Symmetrify V) _ a b) :=
Quotient.eq'
end WeaklyConnectedComponent
variable {V}
-- Without the explicit universe level in `Quiver.{v+1}` Lean comes up with
-- `Quiver.{max u_2 u_3 + 1}`. This causes problems elsewhere, so we write `Quiver.{v+1}`.
/-- A wide subquiver `H` of `Symmetrify V` determines a wide subquiver of `V`, containing an
an arrow `e` if either `e` or its reversal is in `H`. -/
def wideSubquiverSymmetrify (H : WideSubquiver (Symmetrify V)) : WideSubquiver V :=
fun _ _ ↦ { e | H _ _ (PSum.inl e) ∨ H _ _ (PSum.inr e) }
end Quiver
```

#### Kevin Buzzard (Dec 12 2022 at 08:06):

My instinct is that the port should be 1-1 and any refractors should be done after it's complete.

Last updated: Dec 20 2023 at 11:08 UTC