{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:52:17Z","timestamp":1770274337075,"version":"3.49.0"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2017,10,17]],"date-time":"2017-10-17T00:00:00Z","timestamp":1508198400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,1]]},"abstract":"<jats:p>The delay datatype was introduced by Capretta (<jats:italic>Logical Methods in Computer Science<\/jats:italic>, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-L\u00f6f type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad\u2013a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (<jats:italic>Extensional Constructs in Intensional Type Theory<\/jats:italic>, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free \u03c9-complete pointed partial orders (\u03c9cppos).<\/jats:p><jats:p>Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534\u2013549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive\u2013inductive type is the free \u03c9cppo on a type <jats:italic>X<\/jats:italic> essentially by definition; this allowed them to obtain a monad of free \u03c9cppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.<\/jats:p>","DOI":"10.1017\/s0960129517000184","type":"journal-article","created":{"date-parts":[[2017,10,17]],"date-time":"2017-10-17T02:51:42Z","timestamp":1508208702000},"page":"67-92","source":"Crossref","is-referenced-by-count":20,"title":["Quotienting the delay monad by weak bisimilarity"],"prefix":"10.1017","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-8252","authenticated-orcid":false,"given":"JAMES","family":"CHAPMAN","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1297-0579","authenticated-orcid":false,"given":"TARMO","family":"UUSTALU","sequence":"additional","affiliation":[]},{"given":"NICCOL\u00d2","family":"VELTRI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"S0960129517000184_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48167-2_12"},{"key":"S0960129517000184_ref17","first-page":"173","volume-title":"Proceedings of 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013","author":"Kraus","year":"2013"},{"key":"S0960129517000184_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.06.017"},{"key":"S0960129517000184_ref22","first-page":"230","volume-title":"Revised Lectures from Proceedings of the 6th International School on Advanced Functional Programming, AFP 2008","author":"Norell","year":"2009"},{"key":"S0960129517000184_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"S0960129517000184_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129517000184_ref3","first-page":"534","volume-title":"Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2017","author":"Altenkirch","year":"2017"},{"key":"S0960129517000184_ref2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:14)2014"},{"key":"S0960129517000184_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0960129517000184_ref25","volume-title":"Constructivism in Mathematics: An Introduction","author":"Troelstra","year":"1988"},{"key":"S0960129517000184_ref26","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013"},{"key":"S0960129517000184_ref24","unstructured":"Rosolini G. (1986). Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford."},{"key":"S0960129517000184_ref13","volume-title":"CPHS\/BCS Distinguished Dissertations","author":"Hofmann","year":"1997"},{"key":"S0960129517000184_ref6","first-page":"115","volume-title":"Proceedings of 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009","author":"Kennedy","year":"2009"},{"key":"S0960129517000184_ref9","first-page":"117","volume-title":"Proceedings of 28th Conference on the Mathematical Foundations of Program Semantics, MFPS XXVIII","author":"Cockett","year":"2012"},{"key":"S0960129517000184_ref15","first-page":"67","volume-title":"Science of Computer Programming","volume":"37","author":"Hughes","year":"2000"},{"key":"S0960129517000184_ref8","first-page":"95","volume-title":"Selected Papers from Int. Wksh. on Types for Proofs and Programs, TYPES 2002","author":"Chicli","year":"2003"},{"key":"S0960129517000184_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007308"},{"key":"S0960129517000184_ref12","first-page":"183","volume-title":"Proceedings of 31st Conference on Mathematical Foundations of Programming Semantics, MFPS XXXI","author":"Goncharov","year":"2015"},{"key":"S0960129517000184_ref14","first-page":"131","volume-title":"Proceedings of International Conference on Category Theory","author":"Hyland","year":"1990"},{"key":"S0960129517000184_ref19","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxh162"},{"key":"S0960129517000184_ref11","first-page":"21","volume-title":"Proceedings of Wksh. on Domain-Theoretical Methods for Probabilistic Programming","author":"Escard\u00f3","year":"2004"},{"key":"S0960129517000184_ref23","unstructured":"Nuo L. (2015). Quotient types in type theory. PhD thesis, University of Nottingham."},{"key":"S0960129517000184_ref7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"S0960129517000184_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00124-2"},{"key":"S0960129517000184_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005130"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129517000184","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T17:03:25Z","timestamp":1555088605000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129517000184\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,17]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,1]]}},"alternative-id":["S0960129517000184"],"URL":"https:\/\/doi.org\/10.1017\/s0960129517000184","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,17]]}}}