search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

Notation for total space of family of types #150

Open marcbezem opened 2 years ago

marcbezem commented 2 years ago

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 commented 2 years ago 
4.  Tot P
bidundas commented 2 years ago

P invisible squirrel A

Bjorn

On 1 Sept 2022, at 19:13, Daniel R. Grayson @.***> wrote:



  1. 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 commented 2 years ago

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).