Dependent map on quotient: closing the `eq.rec` goal?

Stream: new members

[Rémi Bottinelli]

I'm trying to define the quotient of a groupoid by a normal subgroupoid below (following Bourbaki's Topologie Algébrique), and to do so I need first to define the vertices as a quotient, and then the arrows as another one (see below). I'm getting into troubles when trying to define the identity and composition morphisms, since their types depend on the element(s) on which they are defined.
quot.rec seems to be the correct way to proceed, but then I get stuck trying to prove the "soundness" of my recursion, which involves an eq.rec. Am I off-base, or missing something?
Note that for the identity morphism, I can get around this problem since I can first define a non-dependent lift, but it's not really "pretty" and wouldn't work for the composition without ugly tricks, I believe.

Thanks!

import category_theory.groupoid

open set

namespace category_theory

universes u v

variables {C : Type u}

namespace groupoid

section subgroupoid

variable (G : groupoid C)

@[ext]
structure subgroupoid :=
  (arrws : ∀ (c d : C), set (G.hom c d))
  (inv' : ∀ {c d} {p : G.hom c d} (hp : p ∈ arrws c d),
            groupoid.inv p ∈ arrws d c)
  (mul' : ∀ {c d e} {p} (hp : p ∈ arrws c d) {q} (hq : q ∈ arrws d e),
            p ≫ q ∈ arrws c e)

variable {G}

def is_normal (S : subgroupoid G) : Prop :=
  (∀ c, (𝟙 c) ∈ (S.arrws c c)) ∧  -- S is "wide": all vertices of G are covered
  (∀ {c d} (p : c ⟶ d) (γ : c ⟶ c) (hs : γ ∈ S.arrws c c), ((G.inv p) ≫ γ ≫ p) ∈ (S.arrws d d))


end subgroupoid


section quotient

-- The vertices of the quotient of G by S
def quot_v [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :=
  (quot (λ (c d : C), (S.arrws c d).nonempty))


def quot_v.mk [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) (c : C) : quot_v S Sn:=
  (quot.mk (λ (c d : C), (S.arrws c d).nonempty) c)

def conj  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  (Σ (a b : C), a ⟶ b) → (Σ (a b : C), a ⟶ b) → Prop :=
begin
  rintros ⟨a,b,f⟩ ⟨c,d,g⟩,
  exact ∃ (α ∈ S.arrws a c) (β ∈ S.arrws d b), f = α ≫ g ≫ β
end

@[refl]
lemma conj.refl [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : ∀ F, conj S Sn F F :=
begin
  rintro ⟨a,b,f⟩,
  use [(𝟙 a), Sn.left a, (𝟙 b), Sn.left b],
  simp only [category.comp_id, category.id_comp],
end

@[symm]
lemma conj.symm [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : ∀ F G, conj S Sn F G → conj S Sn G F :=
begin
  rintros ⟨a,b,f⟩ ⟨c,d,g⟩ ⟨α,hα,β,hβ,rfl⟩,
  use [G.inv α, S.inv' hα, G.inv β, S.inv' hβ],
  simp only [category.assoc, comp_inv, category.comp_id],
  rw ←category.assoc,
  simp only [inv_comp, category.id_comp],
end

@[trans]
lemma conj.trans [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  ∀ F G H, conj S Sn F G → conj S Sn G H → conj S Sn F H :=
begin
  rintros ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨a₂,b₂,f₂⟩ ⟨α₀,hα₀,β₀,hβ₀,rfl⟩  ⟨α₁,hα₁,β₁,hβ₁,rfl⟩,
  use [α₀ ≫ α₁, S.mul' hα₀ hα₁, β₁ ≫ β₀, S.mul' hβ₁ hβ₀],
  simp only [category.assoc],
end

def quot_start [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : (quot $ conj S Sn) → (quot_v S Sn) :=
begin
  refine quot.lift _ _,
  { rintro ⟨a,b,f⟩, apply quot_v.mk, exact a,},
  { rintro ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨α,hα,β,hβ,rfl⟩,simp,dsimp [quot_v.mk], apply quot.sound, exact ⟨α,hα⟩,}
end

def quot_end [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : (quot $ conj S Sn) → (quot_v S Sn) :=
begin
  refine quot.lift _ _,
  { rintro ⟨a,b,f⟩, apply quot_v.mk, exact b,},
  { rintro ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨α,hα,β,hβ,rfl⟩,simp,dsimp [quot_v.mk], apply quot.sound, exact ⟨G.inv β,S.inv' hβ⟩,}
end

@[instance]
def quotient_quiver [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  quiver (quot_v S Sn) := ⟨λc d, { F | quot_start S Sn F = c ∧ quot_end S Sn F = d }⟩

def quot_id'  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  (quot $ conj S Sn) :=
begin
  apply quot.lift, rotate,
  { rintro c,
    exact quot.mk (conj S Sn) ⟨c,c,𝟙 c⟩ },
  { rintros c d ⟨f,fS⟩,
    apply quot.sound,
    use [f,fS,G.inv f, S.inv' fS],
    simp only [category.id_comp, comp_inv], }
end

def quotient_id  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  c ⟶ c :=
λ c, ⟨ quot_id' S Sn c, by {dsimp only [quot_id',quot_start,quot_end,quot_v.mk], induction c, simp, simp,}⟩


def quot_id''  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c : quot_v S Sn),  c ⟶ c :=
begin
  refine λ c, c.rec_on _ _,
  { rintro c, dsimp only [quotient_quiver,quot_start,quot_end,quot_v.mk],
    use quot.mk (conj S Sn) ⟨c,c,𝟙 c⟩, split, simp only, simp only, },
  { rintros c d ⟨f,fS⟩,
    have : quot.mk (λ (c d : C), (S.arrws c d).nonempty) c = quot.mk (λ (c d : C), (S.arrws c d).nonempty) d, by
    { apply quot.sound, constructor, use fS,},
    simp,
    sorry,
    }
end


def quot_comp'  [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) : Π (c d e : quot_v S Sn), (c ⟶ d) → (d ⟶ e) → (quot $ conj S Sn) :=
begin
  sorry
end


end quotient


end groupoid
end category_theory

[Junyan Xu]

Several comments:

• Since you've shown that conj is reflexive, symmetric and transitive, you may package them into a docs#setoid instance, and then you can use quotient instead of quot, which allows you access to theorems like docs#quotient.exact that isn't true if the relation you quotient by is not an equivalence relation.
• When defining data, we usually don't destruct an input; instead we use its projections. For example, conj should be defined as λ f g, ∃ (α ∈ S.arrws f.1 g.1) (β ∈ S.arrws g.2.1 f.2.1), f.2.2 = α ≫ g.2.2 ≫ β, and the same applies to quot_start and quot_end; in proofs we don't care though.
• I think the way you construct quot_id and quotient_id is perfectly fine. Not sure why you want to try the approach in quot_id''. The use of quot.rec_on seems exactly what introduces eq.rec that's hard to deal with.
• In order to define quot_comp', I would take the following approach: first convert (c ⟶ d) and (d ⟶ e) which are subtypes of quotient types into quotient types of subtypes using docs#equiv.subtype_quotient_equiv_quotient_subtype, then use quotient.lift₂. You would still need to use choice to pick an arrow from (S.arrws _ _).nonempty to connect the two lifts of d, but this is the best solution I can think of.

[Junyan Xu]

I think it may be easier to simply define the types of arrows in the quotient groupoid as quotients rather than subtypes of quotients; I believe the following is also a valid definition:

def conj' [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) (a b : quot_v S Sn)
  (f g : Σ (c : {c // quot.mk _ c = a}) (d : {d // quot.mk _ d = b}), c.1 ⟶ d.1) : Prop :=
∃ (α ∈ S.arrws f.1.1 g.1.1) (β ∈ S.arrws g.2.1.1 f.2.1.1), f.2.2 = α ≫ g.2.2 ≫ β

def quotient_quiver [G : groupoid C] (S : subgroupoid G) (Sn : is_normal S) :
  quiver (quot_v S Sn) := ⟨λ a b, quot (conj' S Sn a b)⟩

[Rémi Bottinelli]

Thanks for the feedback.
As for your third bullet: It's mostly because I felt that I'd have to deal with this problem of quot.rec_on/eq.rec with quot_comp anyway, and since id is easier than comp, it would help me figure out how to deal with that.
As for your proposal, I thought about something along these lines but couldn't tell if it was useful. Do we agree that your proposal takes care of the conversion mentioned in bullet 4 already?

[Rémi Bottinelli]

But as far as I understand, I can't simply do quotient.lift₂, because the lift needs to have a dependent codomain, so only quot.rec works here.

[Kyle Miller]

@Rémi Bottinelli I haven't dealt with the composition problem, but I have some suggestions for handling the groupoid structure and how to organize taking the vertex quotient

import category_theory.groupoid

open set

namespace category_theory

universes u v

variables (C : Type u)

namespace groupoid

section subgroupoid

variable [groupoid C]

@[ext]
structure subgroupoid (C : Type u) [groupoid C] :=
(arrws : ∀ (c d : C), set (c ⟶ d))
(inv' : ∀ {c d} {p : c ⟶ d} (hp : p ∈ arrws c d),
          groupoid.inv p ∈ arrws d c)
(mul' : ∀ {c d e} {p} (hp : p ∈ arrws c d) {q} (hq : q ∈ arrws d e),
          p ≫ q ∈ arrws c e)

variable {C}

namespace subgroupoid

structure is_normal (S : subgroupoid C) : Prop :=
(wide : ∀ c, 𝟙 c ∈ S.arrws c c)  -- S is "wide": all vertices of G are covered
(conj {c d} (p : c ⟶ d) (γ : c ⟶ c) (hs : γ ∈ S.arrws c c) :
  groupoid.inv p ≫ γ ≫ p ∈ S.arrws d d)

lemma is_normal.arrws_nonempty_refl {S : subgroupoid C} (Sn : S.is_normal) (c : C) :
  (S.arrws c c).nonempty :=
⟨𝟙 c, Sn.wide c⟩

lemma is_normal.arrws_nonempty_symm {S : subgroupoid C} (Sn : S.is_normal)
  {c d : C} : (S.arrws c d).nonempty → (S.arrws d c).nonempty :=
by { rintro ⟨f, hf⟩, exact ⟨groupoid.inv f, S.inv' hf⟩ }

lemma is_normal.arrws_nonempty_trans {S : subgroupoid C} (Sn : S.is_normal)
  {c d e : C} : (S.arrws c d).nonempty → (S.arrws d e).nonempty → (S.arrws c e).nonempty :=
by { rintro ⟨f, hf⟩ ⟨g, hg⟩, exact ⟨f ≫ g, S.mul' hf hg⟩ }

def is_normal.arrws_nonempty_setoid {S : subgroupoid C} (Sn : S.is_normal) : setoid C :=
{ r := λ c d, (S.arrws c d).nonempty,
  iseqv := ⟨Sn.arrws_nonempty_refl,
            λ c d, Sn.arrws_nonempty_symm,
            λ c d e, Sn.arrws_nonempty_trans⟩ }

end subgroupoid

end subgroupoid

section quotient
variables {C} [groupoid C] (S : subgroupoid C) (Sn : S.is_normal)

-- The vertices of the quotient of G by S
@[reducible] def subgroupoid.quot_v := quotient Sn.arrws_nonempty_setoid

def subgroupoid.quot_v_mk (c : C) : S.quot_v Sn := quotient.mk' c

namespace subgroupoid

/-- We don't need Sn in the definition, but it makes it inferrable where it is needed. -/
def conj (Sn : S.is_normal) : (Σ (a b : C), a ⟶ b) → (Σ (a b : C), a ⟶ b) → Prop
| ⟨a, b, f⟩ ⟨c, d, g⟩ := ∃ (α ∈ S.arrws a c) (β ∈ S.arrws d b), f = α ≫ g ≫ β

@[refl]
lemma conj.refl : ∀ F, S.conj Sn F F :=
begin
  rintro ⟨a,b,f⟩,
  use [𝟙 a, Sn.wide a, 𝟙 b, Sn.wide b],
  simp only [category.comp_id, category.id_comp],
end

@[symm]
lemma conj.symm : ∀ F G, S.conj Sn F G → S.conj Sn G F :=
begin
  rintros ⟨a,b,f⟩ ⟨c,d,g⟩ ⟨α,hα,β,hβ,rfl⟩,
  use [groupoid.inv α, S.inv' hα, groupoid.inv β, S.inv' hβ],
  simp only [category.assoc, comp_inv, category.comp_id],
  rw ←category.assoc,
  simp only [inv_comp, category.id_comp],
end

@[trans]
lemma conj.trans : ∀ F G H, conj S Sn F G → conj S Sn G H → conj S Sn F H :=
begin
  rintros ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨a₂,b₂,f₂⟩ ⟨α₀,hα₀,β₀,hβ₀,rfl⟩  ⟨α₁,hα₁,β₁,hβ₁,rfl⟩,
  use [α₀ ≫ α₁, S.mul' hα₀ hα₁, β₁ ≫ β₀, S.mul' hβ₁ hβ₀],
  simp only [category.assoc],
end

def conj_setoid : setoid (Σ (a b : C), a ⟶ b) :=
{ r := S.conj Sn,
  iseqv := ⟨conj.refl _ _, λ _ _, conj.symm _ _ _ _, λ _ _ _, conj.trans _ _ _ _ _⟩ }

@[reducible] def quot_conj := quotient (S.conj_setoid Sn)

def quot_conj_mk {a b : C} (f : a ⟶ b) : S.quot_conj Sn := quotient.mk' ⟨a, b, f⟩

namespace quot_conj
variables {S} {Sn}

protected def start : S.quot_conj Sn → S.quot_v Sn :=
quotient.map' (λ f, f.1) begin
  rintro ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨α,hα,β,hβ,rfl⟩,
  exact ⟨α, hα⟩,
end

protected def «end»  : S.quot_conj Sn → S.quot_v Sn :=
quotient.map' (λ f, f.2.1) begin
  rintro ⟨a₀,b₀,f₀⟩ ⟨a₁,b₁,f₁⟩ ⟨α,hα,β,hβ,rfl⟩,
  exact ⟨groupoid.inv β, S.inv' hβ⟩,
end

end quot_conj

@[simp]
lemma start_mk_eq {a b : C} (f : a ⟶ b) : (S.quot_conj_mk Sn f).start = S.quot_v_mk Sn a := rfl

@[simp]
lemma end_mk_eq {a b : C} (f : a ⟶ b) : (S.quot_conj_mk Sn f).end = S.quot_v_mk Sn b := rfl

instance quot_quiver : quiver (S.quot_v Sn) :=
⟨λ c d, { F : S.quot_conj Sn | F.start = c ∧ F.end = d }⟩

def quot_id (c : quot_v S Sn) : c ⟶ c :=
⟨quotient.lift_on' c (λ c', S.quot_conj_mk Sn (𝟙 c')) begin
  rintro a b ⟨f, hf⟩,
  apply quotient.sound',
  use [f, hf, groupoid.inv f, S.inv' hf],
  simp only [category.id_comp, comp_inv],
end, by exact quotient.ind' (λ _, ⟨rfl, rfl⟩) c⟩

def quot_comp {c d e : quot_v S Sn} : (c ⟶ d) → (d ⟶ e) → (c ⟶ e) :=
begin
  -- should do in a different way
  letI := Sn.arrws_nonempty_setoid,
  refine quotient.rec (λ c', _) _ c,
  refine quotient.rec (λ d', _) _ d,
  refine quotient.rec (λ e', _) _ e,
  rintro ⟨f, hf⟩ ⟨g, hg⟩,
  sorry
end


end subgroupoid
end quotient

end groupoid
end category_theory

[Kyle Miller]

I think Junyan's correct about how the main difficulty is in subtypes of quotients vs quotients of subtypes. It might help to make custom lift functions to deal with dependent types from the objects.

[Rémi Bottinelli]

Thanks for the cleaned-up code. I tried commuting quotients and subtype here but as far as I can tell, it doesn't help with the fact that I need a dependent function.

[Junyan Xu]

@Rémi Bottinelli Here's a full construction of the composition, which should be inserted after

def subgroupoid.quot_v_mk
namespace subgroupoid

in Kyle's code (thanks!). I use my own definition of quotient_quiver to be able to apply quot.lift₂ directly. Surely the resulting type c ⟶ e depends on c and e, but it's still the same type for different choice of elements of the input types c ⟶ d and d ⟶ e, so quot.lift works without problem. (With your original definition of quotient_quiver, the situation is in some sense better, since you're constructing an element in a subtype of a type that doesn't even depend on c and e, however needing to convert from subtype of quotient to quotient of subtype makes it unpleasant to work with.) I might open a PR to put everything about inv into category_theory.groupoid.

def conj {a b c d : C} (f : a ⟶ b) (g : c ⟶ d) : Prop :=
∃ (α ∈ S.arrws a c) (β ∈ S.arrws d b), f = α ≫ g ≫ β

attribute [reassoc] inv_comp comp_inv -- groupoid

lemma conj.refl {a b : C} (f : a ⟶ b) : S.conj f f := ⟨_, Sn.wide _, _, Sn.wide _, by simp⟩

lemma conj.symm {a b c d : C} (f : a ⟶ b) (g : c ⟶ d) : S.conj f g → S.conj g f :=
λ ⟨α, hα, β, hβ, he⟩, ⟨_, S.inv' hα, _, S.inv' hβ, by simp [he]⟩

lemma conj_comm {a b c d : C} (f : a ⟶ b) (g : c ⟶ d) : S.conj f g ↔ S.conj g f :=
⟨conj.symm S f g, conj.symm S g f⟩

lemma conj.trans {a b c d e f : C} (g : a ⟶ b) (h : c ⟶ d) (i : e ⟶ f) :
  S.conj g h → S.conj h i → S.conj g i :=
λ ⟨α₁, hα₁, β₁, hβ₁, he₁⟩ ⟨α₂, hα₂, β₂, hβ₂, he₂⟩,
  ⟨_, S.mul' hα₁ hα₂, _, S.mul' hβ₂ hβ₁, by simp [he₁, he₂]⟩

def conj_setoid (a b : quot_v S Sn) :
  setoid (Σ (c : {c // quot.mk _ c = a}) (d : {d // quot.mk _ d = b}), c.1 ⟶ d.1) :=
{ r := λ f g, S.conj f.2.2 g.2.2,
  iseqv := ⟨λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _⟩ }

lemma conj_comp {a b c d e : C} (f : a ⟶ b) (g : c ⟶ d) {h : d ⟶ e} (hS : h ∈ S.arrws d e) :
  S.conj f (g ≫ h) ↔ S.conj f g :=
⟨λ ⟨α, hα, β, hβ, he⟩, ⟨α, hα, h ≫ β, S.mul' hS hβ, by simp [he]⟩,
 λ ⟨α, hα, β, hβ, he⟩, ⟨α, hα, inv h ≫ β, S.mul' (S.inv' hS) hβ, by simp [he]⟩⟩

lemma conj_comp' {a b c d e : C} (f : a ⟶ b) (g : c ⟶ d) {h : e ⟶ c} (hS : h ∈ S.arrws e c) :
  S.conj f (h ≫ g) ↔ S.conj f g :=
⟨λ ⟨α, hα, β, hβ, he⟩, ⟨α ≫ h, S.mul' hα hS, β, hβ, by simp [he]⟩,
 λ ⟨α, hα, β, hβ, he⟩, ⟨α ≫ inv h, S.mul' hα (S.inv' hS), β, hβ, by simp [he]⟩⟩

@[simp] lemma inv_inv {a b : C} (f : a ⟶ b) : inv (inv f) = f :=
by rw [← category.comp_id (inv (inv f)), ← inv_comp f, inv_comp_assoc]

lemma conj_congr_left {a b c d : C} (f₁ : a ⟶ c) (f₂ : b ⟶ c) (g : c ⟶ d) (h : S.conj f₁ f₂) :
  S.conj (f₁ ≫ g) (f₂ ≫ g) :=
let ⟨α, hα, β, hβ, he⟩ := h in ⟨α, hα, _, Sn.conj g _ hβ, by simp [he]⟩

lemma conj_congr_right {a b c d : C} (f : a ⟶ b) (g₁ : b ⟶ c) (g₂ : b ⟶ d) (h : S.conj g₁ g₂) :
  S.conj (f ≫ g₁) (f ≫ g₂) :=
let ⟨α, hα, β, hβ, he⟩ := h in ⟨_, Sn.conj (groupoid.inv f) _ hα, β, hβ, by simp [he]⟩

@[instance]
def quotient_quiver : quiver (quot_v S Sn) := ⟨λ a b, quotient (conj_setoid S Sn a b)⟩

noncomputable def quot_comp {c d e : quot_v S Sn} : (c ⟶ d) → (d ⟶ e) → (c ⟶ e) :=
begin
  let sm := @nonempty.some_mem,
  refine quot.lift₂ (λ f g, quot.mk _ _) (λ f g₁ g₂ h, _) (λ f₁ f₂ g h, _),
  { letI := Sn.arrws_nonempty_setoid,
    exact ⟨_, _, f.2.2 ≫ (quotient.exact $ f.2.1.2.trans g.1.2.symm).some ≫ g.2.2⟩ },
  all_goals { apply quot.sound, dsimp only [conj_setoid] },
  { apply S.conj_congr_right Sn,
    rw [S.conj_comp' _ _ (sm _), conj_comm, S.conj_comp' _ _ (sm _), conj_comm],
    exact h },
  { simp only [← category.assoc],
    apply S.conj_congr_left Sn,
    rw [S.conj_comp _ _ (sm _), conj_comm, S.conj_comp _ _ (sm _), conj_comm],
    exact h },
end

[Junyan Xu]

Oh I see you actually added four lemmas about groupoids in the free groupoid PR. I think the best thing to do is to first show that groupoid.inv = docs#category_theory.inv, and use the latter everywhere (we already has the is_iso instance), to avoid duplicating the API (docs#category_theory.is_iso.inv_comp etc. already exist). So we should probably open category_theory but not open groupoid (or hide groupoid.inv) to be able to simply write inv.

[Junyan Xu]

see PR #16624

[Rémi Bottinelli]

Thanks a lot! Looking forward to see what I was misunderstanding exactly.

[Rémi Bottinelli]

I think I'm being stupid, but actually, following your approach to the quotient, I feel like now defining id becomes problematic. How would you do it?

[Junyan Xu]

The easy way is to use choice:

noncomputable def quot_id (c : quot_v S Sn) : c ⟶ c :=
quot.mk _ ⟨⟨_, quot.out_eq c⟩, ⟨_, quot.out_eq c⟩, 𝟙 _⟩

or you could also do it computably (albeit more complicated, and I have to adjust the sigma type to a subtype in order to use docs#subtype_quotient_equiv_quotient_subtype):

def sigma_conj_setoid (a b : quot_v S Sn) : setoid (Σ c d : C, c ⟶ d) :=
{ r := λ f g, S.conj f.2.2 g.2.2,
  iseqv := ⟨λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _⟩ }

def conj_setoid' (a b : quot_v S Sn) :
  setoid {f : Σ c d : C, c ⟶ d // quot.mk _ f.1 = a ∧ quot.mk _ f.2.1 = b} :=
{ r := λ f g, S.conj f.1.2.2 g.1.2.2,
  iseqv := ⟨λ _, conj.refl _ Sn _, λ _ _, conj.symm _ _ _, λ _ _ _, conj.trans _ _ _ _⟩ }
-- setoid.comap coe (sigma_conj_setoid S Sn a b) -- need import data.setoid.basic

@[instance]
def quotient_quiver : quiver (quot_v S Sn) := ⟨λ a b, quotient (conj_setoid' S Sn a b)⟩

def quot_id (c : quot_v S Sn) : c ⟶ c :=
begin
  refine @equiv.subtype_quotient_equiv_quotient_subtype _ _ (sigma_conj_setoid S Sn c c)
    (conj_setoid' S Sn c c) (quot.lift _ $ λ f g h, _) (λ _, iff.rfl) (λ f g, iff.rfl) _,
  { obtain ⟨a, ha, b, hb, -⟩ := h, congr' 2; apply quot.sound, exacts [⟨a, ha⟩, ⟨_, S.inv' hb⟩] },
  { refine ⟨quot.lift (λ c, quot.mk _ _) (λ d e h, _) c, _⟩, { exact ⟨c, c, 𝟙 c⟩ },
    { obtain ⟨a, ha⟩ := h, refine quot.sound ⟨a, ha, _, S.inv' ha, by simp⟩ },
    { rcases c, exacts ⟨rfl, rfl⟩ } },
end

/- and you get nice defeq: -/
lemma quot_id_eq (c : C) : quot_id S Sn (quot_v_mk S Sn c) = quot.mk _ ⟨⟨c, c, 𝟙 c⟩, rfl, rfl⟩ := rfl

[Junyan Xu]

Sorry I haven't got a chance to look at your new free groupoid PR carefully yet, but I agree with Joël's comment there.

[Rémi Bottinelli]

Junyan Xu said:

Sorry I haven't got a chance to look at your new free groupoid PR carefully yet, but I agree with Joël's comment there.

No worry, I'm trying to finish the quotient construction in the meantime. It's at the edge of my lean abilities, so I'm advancing very slowly!

[Rémi Bottinelli]

Actually, I think I found a probably easier way to deal with the quotient:
If N is a normal subgroupoid, one should be able to decompose it into V * G where V consists only of the vertex groups of N, and G has at most one arrow per pair of vertices. One can then quotient first by N and then by G:

• Quotienting by N preserves the vertices, so we only need to quotient edges.
• Quotienting then by G preserves arrows: we're just bunching groups together corresponding to squashing vertices.

So, both definitions should be relatively transparent, and they're actually useful by their own I believe.