Constructions of categories of setoids from proof-irrelevant families. (English) Zbl 1390.03013

Palmgren, Erik

Arch. Math. Logic 56, No. 1-2, 51-66 (2017).

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

(1)

\(F(\mathrm{refl}(x))) = \mathrm{id}_{F(x)}\);

(2)

if \(p,q : x =_A y\) then \(F(p) = F(q)\) hence the proof-irrelevance;

(3)

\(F(q) \circ F(p) = F(q \circ p)\) when the compositions are defined.

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 O. Wilander, Log. Methods Comput. Sci. 10, No. 3, Paper No. 25, 14 p. (2014; Zbl 1341.03012); 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.

Reviewer: Marco Benini (Buccinasco)

MSC:

03B15	Higher-order logic; type theory (MSC2010)
18B05	Categories of sets, characterizations
18B15	Embedding theorems, universal categories

Keywords:

Martin-Löf type theory; proof-irrelevance; category

Citations:

Zbl 1241.03005; Zbl 1341.03012; Zbl 1261.03176

Software:

Coq; Agda

References:

[1]	Altenkirch, T.: Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science, pp. 412-421. IEEE Press, Piscataway (1999) · Zbl 1060.03030
[2]	Barthe, G; Capretta, V; Pons, O, Setoids in type theory, J. Funct. Program., 13, 261-293, (2003) · Zbl 1060.03030
[3]	Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967) · Zbl 0183.01503
[4]	Hofmann, M.: Extensional Concepts in Intensional Type Theory. Springer, Berlin (1997)
[5]	Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Sambin, G., Smith, J. (eds.) Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, pp. 83-111. Oxford University Press, New York (1998) · Zbl 0930.03089
[6]	Maietti, ME; Rosolini, G, Quotient completion for the foundation of constructive mathematics, Logica Universalis, 7, 371-402, (2013) · Zbl 1288.03049
[7]	Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf Type Theory. Oxford University Press, Oxford (1990) · Zbl 0744.03029
[8]	Palmgren, E, Proof-relevance of families of setoids and identity in type theory, Arch. Math. Log., 51, 35-47, (2012) · Zbl 1241.03005
[9]	Palmgren, E., Wilander, O.: Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci. 10(3), paper 25 (2014) · Zbl 1341.03012
[10]	Wilander, O, Constructing a small category of setoids, Math. Struct. Comput. Sci., 22, 103-121, (2012) · Zbl 1261.03176