This note studies quotient types in the Calculus of Inductive Constructions (CIC), implemented in the proof assistant coq, and compares their expressivity to that of mathematical quotients. In [Hof95], Martin Hofmann proposes an extension of the Calculus of Constructions (CC) with quotient types which he shows consistent, but notices that they are not sufficient to account for the natural isomorphism θ which exists in set theory between functional spaces $ E \to \frac{F} {R} $ E \to \frac{F} {R} and $ \frac{{E \to F}} {S} $ \frac{{E \to F}} {S} where $ f{\mathbf{ }}Sg{\mathbf{ }}{\text{iff}}{\mathbf{ }}\forall x \in F,{\mathbf{ }}f\left( x \right)Rg\left( x \right) $ f{\mathbf{ }}Sg{\mathbf{ }}{\text{iff}}{\mathbf{ }}\forall x \in F,{\mathbf{ }}f\left( x \right)Rg\left( x \right) . One can thus ask the question to know if it is possible to extend these quotient types to be able to show injectivity and surjectivity of this morphism. We show here that any extension of this kind in Coq with the impredicative sort Set would be contradictory.