# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTodd_Trimble
• CommentTimeAug 22nd 2012

I’ve been adding a large number of details to the material Sridhar had started at tripos and also to partial combinatory algebra.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeAug 22nd 2012
• (edited Aug 22nd 2012)

I have added a bunch of hyperlinks to the entry, and linked to the entry from hyperdoctrine and first-order hyperdoctrine.

Notice, by the way, that in order for the definition/theorem-environments to come out numbered as intended, one needs to stick to the prescribed instiki syntax. Notably it has to be

  +-- {: .num_defn}


  +-- {: .num_def}


which won’t be recognized. Also, it has to be

  +-- {: .num_theorem}
+-- {: .num_remark}


  +-- {: .num_thm}
+-- {: .num_rem}


So I have fixed that.

(I agree that these 3-letter abbreviations would maybe be more systematic, in particular since it is

  +-- {: .num_cor}


  +-- {: .num_corollary}


which is a constant source of me going back to that page and checking if I remember correctly.)

• CommentRowNumber3.
• CommentAuthorAndrew Stacey
• CommentTimeAug 22nd 2012

If this is a major hassle to keep checking, I could find out if it is easy to add “aliases”. I’ve no idea, but it could be investigated.

When I saw the title of this thread, I thought of a different “Tripos” which a few UK-trained mathematicians might still have nightmares about. Probably don’t need a disambiguation page for that, though.

• CommentRowNumber4.
• CommentAuthorZhen Lin
• CommentTimeAug 22nd 2012

I’m sure the pun was completely intended, given how Pitts, Hyland, and Johnstone are all in Cambridge…

• CommentRowNumber5.
• CommentAuthorjim_stasheff
• CommentTimeAug 22nd 2012
Ah, so pun intended! good to know
• CommentRowNumber6.
• CommentAuthorTodd_Trimble
• CommentTimeAug 22nd 2012
• (edited Aug 22nd 2012)

Yeah, it’s both an acronym and a pun, due really to Johnstone I think. Initially (more punning!), tripos stood for “Topos Representing Indexed Partially Ordered Set”. I’m probably going to have to add this to the entry.

Thanks, Urs, for the corrections! Also, I’d like to have anchors for the three examples in the Examples section. I tried to create some; let me see if I can work this out successfully. (Edit: done.)

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeNov 12th 2017

I added to tripos a mention of the weaker notion introduced by Pitts in “Tripos theory in retrospect”, and also the fact that the beta-reduced construction doesn’t seem to rely on the existence of equality predicates either.