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.

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

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

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

]]>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}
```

instead of

```
+-- {: .num_def}
```

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

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

instead of

```
+-- {: .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}
```

instead of

```
+-- {: .num_corollary}
```

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

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

]]>