issue 1576 implemented differently

[rmatthes]

• Require Export UniMath.Tactics.EnsureStructuredProofs. should appear in the files that are root of a dependency tree
• modifies the previous treatment of SubstitutionSystems and Bicategories
• applies the treatment to package PAdics
• the PAdics files were partly in DOS encoding, now in sync with the rest - can irritate diff tools (the tool meld copes with this well)

[nmvdw]

error: *** UniMath/PAdics/lemmas.vo should not require UniMath/Tactics/EnsureStructuredProofs.vo
[35](https://github.com/UniMath/UniMath/actions/runs/3332521688/jobs/5513490860#step:4:36)
error: *** UniMath/Bicategories/Core/Bicat.vo should not require UniMath/Tactics/EnsureStructuredProofs.vo
[36](https://github.com/UniMath/UniMath/actions/runs/3332521688/jobs/5513490860#step:4:37)
2 dependency order errors in package listings

I'm surprised by these errors. For the remainder the PR looks good.

[nmvdw]

The error seems to come from the fact that the package tactics comes after both Bicategories and PAdics. This means that either this file must be put in some other package or Tactics need to be put in front (different way of generating CONTENTS.md).

I think the solution is that this part of MakeFile must be put in a different order:

PACKAGES += Foundations
PACKAGES += MoreFoundations
PACKAGES += Combinatorics
PACKAGES += Algebra
PACKAGES += NumberSystems
PACKAGES += SyntheticHomotopyTheory
PACKAGES += PAdics
PACKAGES += CategoryTheory
PACKAGES += Bicategories
PACKAGES += Ktheory
PACKAGES += Topology
PACKAGES += RealNumbers
PACKAGES += Tactics
PACKAGES += SubstitutionSystems
PACKAGES += Folds
PACKAGES += HomologicalAlgebra
PACKAGES += AlgebraicGeometry
PACKAGES += Paradoxes
PACKAGES += Induction

More precisely, PACKAGES += Tactics must be put right after Algebra.

The alternative solution is that the relevant gets put in MoreFoundations, but that might cause more problems than it solves (Require Import MoreFoundations.All would then cause it to be applied in possibly too many cases).

[rmatthes]

Sorry for not having checked this - I had only compiled the library before the commit.

[nmvdw]

It seems like we also need to implement this change in the relevant subrepositories, because now the error is at TypeTheory.

The relevant file (https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/Initiality/SyntacticCategory.v) contains Require UniMath.PAdics.lemmas.
PAdics.lemmas is also imported in https://github.com/UniMath/TypeTheory/blob/master/TypeTheory/Initiality/InterpretationLemmas.v, and for the same lemma.

I do think it's good to merge this PR soon.
So there are two options:

• No let PAdics import StructuredProofs for now.
• Move the lemma to another file (in MoreFoundations for example)

Lemma setquotprpathsandR { X : UU } ( R : eqrel X ) :
  forall x y : X, setquotpr R x = setquotpr R y -> R x y.
Proof.
  intros.
  assert ( pr1 ( setquotpr R x ) y ) as i.
  { assert ( pr1 ( setquotpr R y ) y ) as i0.
    { unfold setquotpr. simpl. apply (pr2 (pr1 (pr2 R))). }
    destruct X0. assumption.
  }
  apply i.
Defined.

When looking further, it seems that setquotprpathsandR already is in Foundations.Sets:

UniMath/UniMath/Foundations/Sets.v

Line 1711 in f358cf5

Theorem weqpathsinsetquot {X : UU} (R : eqrel X) (x x' : X) :

[benediktahrens]

@nmvdw @rmatthes : if I understand correctly, @nmvdw is suggesting a change (simplification) to UniMath and TypeTheory. This suggestion is currently only in the comment to a merged PR. Could you file issues to the relevant repositories, pointing to the comment above?