Constructions of categories of setoids from proof-irrelevant families (Q512135)

The paper illustrates two categories of setoids with equality on objects, showing they are isomorphic within intensional Martin-Löf type theory. Both categories are constructed from a fixed proof-irrelevant family of setoids, and they differ by the way in which arrows are defined. It is worth reminding that a proof-irrelevant family \(F\) of setoids over a setoid \(A\) is a map associating to each \(a \in A\) a setoid \(F(a)\), and to each \(p : x =_A y\) an extensional function \(F(p): F(x) \to F(y)\), the transportation function, such that {\parindent=0.6cm \begin{itemize}\item[(1)] \(F(\mathrm{refl}(x))) = \mathrm{id}_{F(x)}\); \item[(2)] if \(p,q : x =_A y\) then \(F(p) = F(q)\) hence the proof-irrelevance; \item[(3)] \(F(q) \circ F(p) = F(q \circ p)\) when the compositions are defined. \end{itemize}} Both the examined categories' objects form the index setoid, whereas the first category has triples \((a,b,f: F(a) \to F(b))\) as arrows, with \(f\) an extensional function; in the second category arrows are triples \((a,b, R \to \Sigma(I,F)^2)\) where \(R\) is a total relation between the subobjects \(F(a), F(b)\) included in \(\Sigma(I,F)\) of the setoid sum of the family. Clearly, the first category identifies arrows up to transportation maps, while the second one is simpler to use as the transportation maps disappear. The construction of the first category may be generalised to show that the full image of a category along an E-functor into an E-category is a category. The clearly written paper follows [the author, ibid. 51, No. 1--2, 35--47 (2012; Zbl 1241.03005); with \textit{O. Wilander}, Log. Methods Comput. Sci. 10, No. 3, Paper No. 25, 14 p. (2014; Zbl 1341.03012); \textit{O. Wilander}, Math. Struct. Comput. Sci. 22, No. 1, 103--121 (2012; Zbl 1261.03176)] in the text, and deepens the previous results. It is of interest to those working on the fundamental notion of equality in intensional type theory, especially considering the contribution as part of a series of subsequent articles describing ongoing research.