Notation for total space of family of types

[marcbezem]

Possible notations for total space of family of types P : A -> U:

1. \hat P
2. P\uparrow A, possibly simplified to simply P\uparrow (since A can be read off from the type of P)
3. no special notation, always write the Sigma-type

(edited to \uparrow for "lying over A")

[DanGrayson]

4.  Tot P

[bidundas]

P invisible squirrel A Bjorn On 1 Sept 2022, at 19:13, Daniel R. Grayson ***@***.***> wrote:  4. Tot P — Reply to this email directly, view it on GitHub<#150 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AKO2SK4MFRPX6Q5GIL2XCRTV4DPZXANCNFSM6AAAAAAQCRELCI>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[marcbezem]

I vote for Dan's 4. Tot P, with the understanding that one can also use the full Sigma-type whenever useful (this holds for all abbreviations).