Quotient category

[barrettj12]

No description provided.

[mortberg]

I had some suggested changes, but then I remembered your issue which answered my questions: #656

I think all of those lemmas should be generalized and I don't think there is a deep reason they are as they currently are. I would suggest you make the generalizations to the set quotient code and then rewrite the quotient category code in this PR.

[barrettj12]

Okay, so I generalised elimProp2, elimProp3, elimContr2 and rec2 in SetQuotients.Properties, and then could make my proofs significantly shorter in Categories.Constructions.Quotient.

I decided not to mess with setQuotUniversal2Iso/setQuotBinOp, as I would have had to add extra arguments, and I figure that would be a huge pain.

However, now when I try to compile Algebra.CommRing.Localisation.UniversalProperty, I get an error:

Failed to solve the following constraints:
  Resolve instance argument _1835 : _r_1834 ∈ Aˣ
  Candidates
    _ :
      Σ (Cubical.Algebra.CommRing.Properties.Units.R A')
      (λ r' → fst φ s ·A r' ≡ 1a)
    _ :
      Σ (Cubical.Algebra.CommRing.Properties.Units.R A')
      (λ r' → fst φ s ⁻¹ ·A r' ≡ 1a)
    (stuck)
  _1835 .fst = PathToS⁻¹R.φS⊆Aˣ cond s s∈S' .fst : fst A'
    (blocked on _1835)

I suppose this wasn't happening before, so I must have broken something?

[ecavallo]

Oops, we did the same thing at the same time: #660

[barrettj12]

Oops, we did the same thing at the same time: #660

My bad, should have seen that you self-assigned it. Yours looks more extensive anyway, I'll see if I can merge it in to mine. Does everything compile okay?

[ecavallo]

Everything worked for me, though we'll see what the CI thinks... I'll see if I can find out what's happening with those instance arguments.

[barrettj12]

However, now when I try to compile Algebra.CommRing.Localisation.UniversalProperty, I get an error:

Well, the CI on this PR just passed, so I'm not sure why I'm getting this error locally. Maybe I'm using a different version of Agda.

[ecavallo]

I tried locally myself and also had no problem, so that might be it.

[mortberg]

I merged #660 now. Please fix the conflicts and use the new lemmas in this PR. Please @ me when this is done and I'll take a look

[barrettj12]

@mortberg should all be good now.

[mortberg]

The proofs look really nice now! I'll merge on the CI is finished