Re: _"(I think) we're perfectly happy to informally have P : Prop be both the pair and the coersion to P : Type"_

[marcbezem]

Re: "(I think) we're perfectly happy to informally have P : Prop be both the pair and the coersion to P : Type"

Currently, a proposition is neither of those things -- currently it's a type that satisfies a property.

Re: "A wrapper inductive type with one constructor with the Σ-type as domain seems too complicated."and "That my whole point, Σ-types are wrappers and we should not need an extra wrapper around them!"

That's simpler than the other way, because one doesn't have to discuss the properties of Σ-types twice.

Re: "The constructor and B form a pair of functions that are each others' inverse up to definitional equality."and "We could say once and for all that mkT and its inverse are inverse in a strong sense (up to definitional equality)"

This is not true in Coq -- there you need to examine cases to show that wrap (unwrap x) = x.

Originally posted by @DanGrayson in https://github.com/UniMath/SymmetryBook/issues/45#issuecomment-605499870

[DanGrayson]

I guess the point of this issue is to resolve the tension in the text between the definition of "proposition" and the elements of the type of propositions, which are pairs, not propositions.

By the way, as Ulrik has remarked, in Coq one can get the η-rule to be valid for such wrappers by using "Record", with primitive projections turned on. That's how UniMath gets the η-rule to apply to pairs. (My final remark above about examining cases was the case for where the wrapper type is a new inductive type.)

UniMath is conservative, so we may not want to add this wrapper to UniMath itself, but perhaps it is time to start formalizing the book anyway, in a separate UniMath repository .

[DanGrayson]

Reopening, as we should do something about this.

One idea: coercions in both directions. I.e., if P is a type and p is a proof that it is a proposition, then in a context where an element of the type of propositions is needed, we'll let silently replace P by (P,p), and conversely, if Q is an element of the type of propositions, then in a context where a type is needed, we'll silently replace Q by π₁Q.

[DanGrayson]

Bidirectional coercions might work for pointed types, too. If we are in a context where a pointed type is required, then we'll silently replace S¹ by (S¹,•). If X is a pointed type, and we are in a context where a type is needed, we'll silently replace X by π₁X (as we already do)

[UlrikBuchholtz]

For subtypes, I like the bidirectional silent promotion/demotion approach you mention. (I think it's only technically a coercion in the demotion direction, where there's a map (fst).)

For pointedness, it's a bit dangerous since the identity types are different. (This is why we have the \div subscripts.) One approach is to always write a * subscript instead when the pointedness needs to be taken into account. I.e., if X is a pointed type, then Aut(X) is the automorphism infinity-group of the underlying type, while Aut_*(X) is the automorphism (infinity) group of X as a pointed type. This is along the lines of what @pierrecagne has been using in the recent work on abelian groups, I think. (Where X = Y is the identity type of underlying types, while X =_* Y is the identity type of pointed types.)

[DanGrayson]

That's a good point The problem with X=Y is that X should be an element of a type, and everything is already an element of a type, which leads me to believe that X=Y should never force a coercion.

What if we say that X=Y involves coercion never, and X =_* Y coerces from types to pointed types, if necessary? The difference between this and what you said is that when X and Y are pointed types, X=Y does not discard the points. We already have notation for discarding basepoints, so we could just use that, when needed.

I don't know ...

[UlrikBuchholtz]

From the README file we have a convention of trying to be informal whenever possible. As such, I think it's hard to have different names for (global) pointed types and their underlying types. (Who could remember whether the circle is “officially” the type or the pointed type?)

And all globally defined types except False will be pointed, anyway.