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 GitHubhttps://github.com/UniMath/SymmetryBook/issues/150#issuecomment-1234559494, or unsubscribehttps://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).