[FOM] theory of cardinals in HOL?

[Andrei Popescu]

Hello, 

If I am not mistaking, cardinals are usually presented in textbooks in a set-theoretic (typically ZF) setting and their theory is constructed basing on ordinals, in turn based on the membership relation.   On the other hand, for my work I needed to employ cardinals within Higher-Order Logic with Infinity and Choice -- some of the theory does seem to go through without using ordinals (and their proper class), but appealing to well-orders instead.  However, I could not find references  to a development of the basic theory of cardinals in this (or a similar) setting. 

Thank you in advance for any such references, 
   Andrei Popescu