We have been working with "levels of signatures" and thereby been puzzled about the way type theory seems to have alternate solutions for Church's 'o' type which appears in his 1940 paper. There seems to a "consensus in intuition" about Church's 'iota' type, but indeed, the 'o' type has been treated differently, even by the same authors over times. Below I try to express my point and I need to choose context and language in order to make myself as clear as possible. I choose notation in Agda for this purpose. I was reading the reference manual of Agda, and the "inductive data type declaration". I looks to me that it mixes "levels of signatures". Similarly, type theory in general, including lambda-calculus, Martin-L??f's type theory, and Homotopy Type Theory, mixes levels of signatures, or simply doesn't care about that mixture. It is almost like making the 'o' "untyped". The declaration data Nat : Set where zero : Nat suc : Nat ??? Nat defines not just the ordinary Sigma_NAT = (S, Omega) signature, where S = {Nat} and Omega is zero : Nat suc : Nat ??? Nat but it also says that "Nat is Set". This "Set" should then be what Church denoted as iota in his 1940 paper. Then it seems to me as '???' in suc : Nat ??? Nat is not the same '???' as in add : Nat ??? Nat ??? Nat where the latter is a lambda term on "another level" as compared to the former. In the latter, the '???' is the "function type constructor", which is an operator on the level of signatures where 'Set', i.e., Church's iota resides. Denoting this type constructor as '==>', I would have ==> : Set ??? Set on the signature level residing "between" the "primitive level" and the "lambda level". This formalization of "levels of signatures" http://www.glioc.com/files_glioc/ModernEyesOnLambdaCalculus.pdf requires a strict definition of the category of signatures, and a formal construction of term monads: http://www.sciencedirect.com/science/article/pii/S0165011413000997 Generally, I feel 'o' is hard because it reflects "sentence", not "term". A term has a type given its construction from operators using sorts, but a sentence "having a sort" is another story. Terms involve possibilities for composable substitutions, whereas sentences do not allow for composable "substition" because sentence functors are "non-monadic". Term functors are monadic. I wonder if anybody would care to comment. Best regards, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund Skype patrikeklund Virtual office: https://connect.sunet.se/patrikeklund/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]