Paper announcement: Dependently Typed Records

The following submitted paper is available at URL

Comments and suggestions are welcome.

	 -- Randy Pollack
Dependently Typed Records for Representing Mathematical Structure
			  Randy Pollack

A notion of dependently typed records is developed naturally from
inductively definable Sigma types.  I consider features such as
labels, coercive subtyping, manifest types, and a "with" notation, and
compare with some existing literature w.r.t. these features.