On Tue, Apr 08, 2014 at 12:43:26PM +1200, W.Taylor at math.canterbury.ac.nz wrote: > There is also the matter of automorphisms, which might not even exist > under this view! > > - Bill Taylor I find the structure of the identify types to be extremely tricky. But an identity type of an object to itself would contain the automorphisms. -- hendrik