Issue with characterizing Sg(A, X)

[ssomayyajula]

In this definition, I'm attempting to show the inductive character of Sg(A, X) i.e. theorem 1.14 in Cliff Bergman's book. This involves inspecting a sequence of elements in X along with evidence that they are members of Y to determine n such that each element is in X n. This apparently requires elimination from Prop to Type, which is verboten; @williamdemeo might remember a similar situation involving the recovery of the preimage of a function from its image.

Basically, this all comes down to the standard library committing to Prop in certain places when really they should be using Sort and let the user declare proof irrelevance at their leisure.

Should we refactor the codebase to work with Sort, use choice, or do something else?

[williamdemeo]

Seems to me we want Sort. It would be nice if we could do this all (or most of it) constructively, and avoid choice, but I'm not sure whether this is possible or realistic.

[williamdemeo]

On the other hand, refactoring the codebase seems a bit extreme. Should we aim for compatibility with the existing codebase?

[williamdemeo]

If by "refactoring the codebase" you mean create all new types (e.g., for set, etc), then that shouldn't present a compatibility issue.