Ulrik Buchholtz
Ulrik Buchholtz
Another way to do it via a hook: ``` (add-hook 'TeX-mode-hook '(lambda () (setq TeX-command-default "LatexMk"))) ```
Well, a subset is the *pair* of the Σ-type and the inclusion. I added a footnote for now (in e983fca), but feel free to rephrase the definition. Lemma 2.22.4(a) (lem:Prop-Set-pointed-families)...
Well, the groupoid of types with an injection into *A* is a set, and is already equivalent/isomorphic to the set of characteristic functions *A*→Prop. (Here, I'll pretend I don't know...
> Pretending that you don’t know what a skeleton is _can_ ruin these things... The argument is that when choosing between equivalent types modelling a categorical notion one would prefer...
> This is not about mathematics, this is about words. Even in a univalent universe we do tend to have different names for differently constructed types, also when they are...
OK, I will implement this as described [above](https://github.com/UniMath/SymmetryBook/issues/73#issuecomment-633125485).
The definition of injection should be moved to this section too.
This is now implemented in 94e489e. However, it now necessitates some rewriting in Sec. 2.23 (sec:typefam), so I'm leaving the issue open for this.
I see this issue is still open, which is apropos of today's discussion. Currently, we say after Cor. 2.19.7 that { t : T | P(t) } is a subset....
Re “In ordinary sets”, I like your re-phrasing, Dan, also without the “In a certain sense”. Re Def. 2.19.5, it's simple if we assume propositional resizing, so we can mention...