# Model for the type-theoretic axiom of choice in Coq.

This is the request for references.

It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent.

It is also know that there is a double-negation Godel-Gentzen translation from classical logic to intuitionistic. (So we can prove something in IZF.)

Does exist a similar result about CIC with axiom of choice? By CIC I mean the Calculus of Inductive Constructions, the system which The Coq proof assistant is based on.

Does exist a model of CIC+choice inside CIC? Where can I learn about it?

Definition choice :=
forall (A B : Type) (P : A -> B -> Prop),
(forall a : A, exists b : B, P a b) ->
exists f : A -> B, forall a : A, P a (f a).

• Maybe Benjamin Werner's paper "Sets in types, types in sets" is a good reading. – Taroccoesbrocco Nov 1 '18 at 9:29
• Isn't that the form of the axiom of choice that's actually provable in a dependent type theory like CIC? – Malice Vidrine Nov 1 '18 at 19:13
• I don't know exactly, but I think that is not, because otherwise why would it be in the library github.com/coq-contribs/zfc ? (see Replacement.v) – ged Nov 2 '18 at 7:12