-(*i $Id: Eqdep.v,v 1.10 2004/01/27 14:37:30 herbelin Exp $ i*)
+(*#***********************************************************************)
+
+(*i $Id: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
(*#* This file defines dependent equality and shows its equivalence with
equality on dependent pairs (inhabiting sigma-types). It axiomatizes
(*#* This file defines dependent equality and shows its equivalence with
equality on dependent pairs (inhabiting sigma-types). It axiomatizes
[2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
Proceedings of the meeting Twenty-five years of constructive
type theory, Venice, Oxford University Press, 1998
[2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
Proceedings of the meeting Twenty-five years of constructive
type theory, Venice, Oxford University Press, 1998