BedrockModels of ZF and ZFC
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA bare structure becomes a model of set theory by supplying witnesses for the ZF axioms. This chapter develops that road in stages: it says what it means for a set to realize a class, proves realizers unique from an explicit extensionality argument, introduces a description operator that reads a set back off its unique existence, and assembles the axioms into a record. It closes by extending a ZF model to ZFC with the axiom of choice.
Nothing in a bare structure yet deserves the name set theory. Its membership relation need not admit an empty set, need not pair two elements, and need not gather the subsets of anything. What a universe of sets must provide is exactly what the axioms of ZF say, and this chapter states them. A model of ZF is a structure whose fields supply the axioms, so "𝒮 satisfies ZF" means precisely that such a witness exists at 𝒮.
The setting is fixed once here: equality and membership in 𝒮 take values in hProp ℓ, so every such assertion is a proposition, and the module runs entirely at one universe level ℓ with its axioms living in Type (ℓ-suc ℓ).
The module signature says what kind of thing will be studied: 𝒮 is a ZFStructure whose truth values are propositions, that is, a structure over hProp ℓ. Two consequences follow immediately. First, the structure's equality ≈ˢ and membership ∈ˢ return propositions with underlying types, so membership claims in this chapter are things one can inhabit with proofs. Second, the parameter {ℓ} is a universe level, and it stays fixed throughout: the carrier S lives in Type ℓ, while statements quantifying over all subsets of S, such as the axioms themselves, will land in Type (ℓ-suc ℓ).
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure; module hPropStructure ) module FOL.ZFModel {ℓ} (𝒮 : ZFStructure ℓ) where
The axioms assert facts directly in hProp. Their constant interpretation is the canonical one from the semantics chapter: the constant domain is the carrier itself and the interpretation is id, so a constant appearing in a formula simply is the set it names.
The working vocabulary for the axioms is assembled here. The syntax chapter supplies Formula, the membership symbol ∈̇, and the constructors var and con; separation and replacement will take formulas as genuine inputs. The semantics chapter contributes the module At, which fixes a constant interpretation and exposes satisfaction for formulas at it. From the host library come Σ≡Prop, used to reduce a path of dependent pairs whose second components are propositions, the type WellFounded of well-foundedness that regularity will record, the empty type Empty.⊥, and propositional truncation ∥_∥₁ for the axiom of choice.
open import FOL.Syntax using ( Formula; var; con; _∈̇_ ) open import FOL.Semantics 𝒮 using ( module At ) open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Induction.WellFounded using ( WellFounded ) import Cubical.Data.Empty as Empty
Two openings put the structure and satisfaction names into scope; the direct hProp operations are already supplied by the prelude. Opening hPropStructure 𝒮 brings the structure's carrier S, its h-set certificate, and the two truth-valued relations ≈ˢ and ∈ˢ, together with the Type-valued reading ∈ᵗ of membership. Finally, opening At S id instantiates the satisfaction relation _⊨_ at the canonical constant interpretation, where a constant denotes itself, so a free variable slot in a formula is read as membership of a specific set.
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁ ) open hPropStructure 𝒮 open At S id using ( _⊨_ )
Realizing a class as a set
Nearly every axiom to come has the same shape: there is a set whose members are exactly the so-and-so. Pin down the "so-and-so" first. A class is a propositional predicate on the carrier, S → hProp ℓ: something whose membership can be stated, with no promise that any set collects it. (Classes have already appeared in disguise: the restriction 𝒮 ↾ M of the structure chapter cuts along exactly such an M.) This section defines when a set realizes a class, observes that realization is itself a proposition, and packages the two together.
The definition of realization is deliberately pointwise. IsSetOf Q b holds when for every element x of the carrier, the proposition x ∈ˢ b is equal, as an element of hProp ℓ, to the class value Q x. There is no formula, no syntax, and no reduction here: the comparison is direct equality of truth values. This type lives in Type (ℓ-suc ℓ) because it quantifies over all of S, matching where the axioms themselves will live.
IsSetOf : (S → hProp ℓ) → S → Type (ℓ-suc ℓ) IsSetOf Q b = (x : S) → (x ∈ˢ b) ≡ Q x isPropIsSetOf : (Q : S → hProp ℓ) (b : S) → isProp (IsSetOf Q b) isPropIsSetOf Q b = isPropΠ (λ x → isSetHProp _ _) SetOf : (S → hProp ℓ) → Type (ℓ-suc ℓ)
That realization is propositional, not a heavier piece of data, is checked now. The function type (x : S) → (x ∈ˢ b) ≡ Q x is a proposition precisely because each fiber is: hProp ℓ is hProp ℓ, and isSetHProp says the type of paths between two propositions packed in hProp is an h-set, so its identity types are propositions; isPropΠ lifts the pointwise fact to the whole function type. Hence SetOf Q, a dependent pair of a candidate set b and evidence IsSetOf Q b, still has propositional second components, a fact used repeatedly later.
SetOf Q = Σ[ b ∈ S ] IsSetOf Q b
How many realizers can one class have? Under extensionality (sets with the same members are equal; it will be the first field of the record) the answer is at most one, in the strong, structural sense: any single realizer makes the whole type of realizers contractible. The lemma takes extensionality as an explicit input, because the record that will provide it has not been defined yet.
Given a realizer (b , sp) of the class Q, the contraction sends any other realizer (b' , sp') to a path into it. The path in the first component is extensionality applied to λ x → sp x ∙ sym (sp' x): at each x, the two specifications give paths x ∈ˢ b ≡ Q x and x ∈ˢ b' ≡ Q x, and composing the first with the reverse of the second yields x ∈ˢ b ≡ x ∈ˢ b', exactly what extensionality turns into b ≡ b'. The second component is disposed of by Σ≡Prop, which is legitimate because isPropIsSetOf says the specifications of any two realizers are equal. Note the argument shape: the class Q and one realizer are explicit inputs, so the conclusion is literally that the type SetOf Q is contractible with the given realizer as center.
setOf-unique : ({a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b) → (Q : S → hProp ℓ) → SetOf Q → isContr (SetOf Q) setOf-unique ext Q (b , sp) = (b , sp) , λ { (b' , sp') → Σ≡Prop (isPropIsSetOf Q) (ext (λ x → sp x ∙ sym (sp' x))) }
The description operator
isContr is the host's unique existence: it packages a center together with the data contracting every element to that center. So isContr (SetOf Q) reads: there is exactly one set of the Qs, with the center supplying a canonical witness outright. Every existence axiom below takes this form, and the payoff is immediate: given unique existence, "the set such that" is a projection. No separate classical description axiom is needed, because the center of a contraction is already data.
The operator ℩ takes a contraction proof of SetOf Q and returns its center's first component, an element of S: with isContr A packaged as a center together with a contraction, c .fst is the center, and one more projection reaches the set itself. This is where a classical treatment would invoke a description axiom; here the passage from unique existence to a witness is pure data extraction, and it is why every axiom below is stated with isContr rather than as a truncated existence.
℩ : {Q : S → hProp ℓ} → isContr (SetOf Q) → S ℩ c = c .fst .fst
The extracted set would be useless without a way to read back what its members are, and that reading is again a projection: ℩-spec c is the specification carried by the center, that is, the second component of the first component of the contraction. Together the two say: the unique set of the Qs exists, and ℩ hands you that set together with the certificate x ∈ˢ (℩ c) ≡ Q x. Every derived operation in the next sections consists of applying ℩ to an axiom field and quoting ℩-spec as its specification.
℩-spec : {Q : S → hProp ℓ} (c : isContr (SetOf Q)) → IsSetOf Q (℩ c) ℩-spec c = c .fst .snd
Subsets
One derived relation completes the vocabulary: a ⊆ˢ b when every member of a is a member of b. This is extensionality's defining comparison, read as a truth value rather than as a hypothesis of a theorem. Unlike the axioms, which will return sets, it lives in hProp ℓ, and it is stated with the direct hProp universal quantifier rather than a host function type. The power set field and the choice-set form of the axiom of choice are phrased with it.
The definition uses the direct hProp quantifier ∀[ x ] P x, to conjoin the implications x ∈ˢ a ⇒ x ∈ˢ b over all x in the carrier. Staying inside hProp ℓ matters: the result is a truth value of the structure, comparable and combinable with the other connectives, whereas a metalevel function type would not be. The Type-valued underlying implication is available too, since each (x ∈ˢ a) ⇒ (x ∈ˢ b) in hProp has an underlying type, but the definition keeps everything truth-valued.
_⊆ˢ_ : S → S → hProp ℓ a ⊆ˢ b = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ (x ∈ˢ b)
The notation a ⊆ˢ b will be used inside the power-set axiom and in later arguments. Its precedence is fixed here so formulas containing membership, equality, and subset have an unambiguous reading.
infix 20 _⊆ˢ_
The axioms, as a record
Here is the heart of the chapter. The fields group into three kinds. First, extensionality and the existence axioms: empty set, pairing, union, separation, replacement, power set, each in the unique-existence form just prepared, so each yields its set through ℩ (infinity joins later). Second, the two formula schemas: separation and replacement take a Formula S 1 or Formula S 2 and interpret it with the satisfaction relation of the semantics chapter, so the language built in the first-order logic chapters does real work here. The restriction is explicit: these fields range over encoded first-order formulas, rather than arbitrary host predicates S → hProp ℓ. Thus every instance used here comes with object-language syntax and is interpreted by the satisfaction relation. Third, regularity: well-foundedness of the Type-valued membership relation, recorded as WellFounded _∈ᵗ_ from the host library. The next section explains why this axiom is stated at the meta level while the others live inside the structure.
The record is a proposition-valued structure plus the guarantees the axioms demand, and it itself lives in Type (ℓ-suc ℓ) because its fields quantify over all of S. The first two fields are not of the unique-existence form. Extensionality is the implication from pointwise agreement of membership truth values to a path a ≡ b, exactly the hypothesis that made setOf-unique work. Regularity takes WellFounded _∈ᵗ_, well-foundedness of the Type-valued membership: this supplies Acc data for every element and thereby supports recursion and induction along membership. The remaining fields each assert isContr (SetOf Q) for a class Q.
record isZFModel : Type (ℓ-suc ℓ) where field extensional : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b regularity : WellFounded _∈ᵗ_ hasEmpty : isContr (SetOf (λ _ → ⊥))
Reading each class back into words recovers the textbook statements. Nothing realizes ⊥, so the empty set is the unique set realizing the constantly-false class. The pair of a and b realizes the class of sets structurally equal to a or to b, joined by the direct hProp disjunction ⊔. The union of a realizes the class of sets x that are members of some member y of a, conjoined by ⊓ and existentially gathered by ∃[ x ] P x. Separation, the first formula-consuming field, keeps exactly those members x of a satisfying φ: the class is the conjunction of membership in a with the satisfaction of φ at the one-element environment x ∷ [], whose single entry fills the only free-variable slot of a Formula S 1.
hasPair : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b))) hasUnion : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y))) hasSeparation : (a : S) (φ : Formula S 1) → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))) hasReplacement : (a : S) (φ : Formula S 2)
Replacement is the longest field and carries a hypothesis of its own. It takes a Formula S 2, whose two free-variable slots are read in the order given by the environment y ∷ x ∷ []: first the output value, then the input. The hypothesis says φ is functional on a: for every member x of a there is exactly one y satisfying φ, exactly-oneness being the isContr of the type of such y. Under that hypothesis the field asserts unique existence of the image, the set of y that stand in the relation φ to some member of a. Note what it does not assert: without the functionality hypothesis the field makes no claim at all, mirroring the classical restriction of replacement to functional formulas. Finally, the power set of a realizes the class of subsets, using the derived relation ⊆ˢ from the previous section.
→ ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))) hasPower : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
Read each λ back into words and the familiar statements reappear. Nothing realizes ⊥, so hasEmpty is the empty set. The pair's members are whatever equals a or b; the union's members are the members of members. Separation keeps those members of a that satisfy φ (the environment x ∷ [] plugs the sole free variable). Replacement first asks φ to be functional on a, one output per input in the isContr sense, then collects the outputs. The power set's members are the subsets.
Why regularity lives at the meta level
Every other axiom speaks either the object language or plain membership; regularity alone reaches for the host's notion of well-foundedness. The classical reason is that no first-order sentence expresses external well-foundedness: by the compactness theorem of classical model theory, any sentence true in exactly the well-founded structures would also hold in a structure carrying an infinite descending ∈-chain, since every finite fragment of the extended theory (a fresh constant chain $a_{n+1} \in a_n$) has a model. The book tells this argument but does not depend on it, and compactness is not developed here. The practical reason, visible in the type WellFounded _∈ᵗ_ itself, is what this interface buys: well-foundedness as explicit data supports recursion and induction along membership. What is surrendered is that the condition is no longer visible to first-order formulas; this chapter makes no claim about how much that matters beyond what is proved below.
The derived operations
Now ℩ turns each unique existence into an operation, and ℩-spec turns it into its specification; every specification below is literally one projection. The union of a pair gives binary union, and binary union gives the successor a ⁺ = a ∪ {a} (the pair of a with itself is the singleton): this is von Neumann's step from one set to the next, the step the axiom of infinity will later use.
Inside the record, each field becomes an operation by applying ℩ to it. The empty set is ℩ hasEmpty, and the pairing operation pair a b applies ℩ to the pairing certificate at the specific a and b. Each such application is justified because the fields provide isContr (SetOf _), which is precisely the input type of ℩. The specification pair-spec is not a new proof at all: it quotes ℩-spec at the same field, and its statement is exactly the realization assertion, that x ∈ˢ pair a b equals the disjunction (x ≈ˢ a) ⊔ (x ≈ˢ b) for every x.
∅ : S ∅ = ℩ hasEmpty pair : S → S → S pair a b = ℩ (hasPair a b) pair-spec : ∀ a b → IsSetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)) (pair a b)
The union operation ⋃ a extracts the union certificate of a, and binary union is defined from it: a ∪ b is the union of the pair pair a b, which is exactly the set whose members are the members of a together with the members of b. No separate axiom is spent on binary union; it is a composite of pairing and union. Note the definition's direction: ∪ is built from ⋃ applied to a pair, not the reverse.
pair-spec a b = ℩-spec (hasPair a b) ⋃ : S → S ⋃ a = ℩ (hasUnion a) _∪_ : S → S → S a ∪ b = ⋃ (pair a b)
Separation becomes an operation in the formula itself: separate a φ applies ℩ to the separation certificate at a and the formula φ, so the resulting set depends on a piece of object-language syntax. Its specification again quotes ℩-spec verbatim, giving x ∈ˢ separate a φ ≡ (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ) for every x: membership combines belonging to a with satisfying φ. The power set operation 𝒫 a extracts the power set certificate, and its members will be read off, via the class it realizes, as exactly the subsets of a.
separate : (a : S) → Formula S 1 → S separate a φ = ℩ (hasSeparation a φ) separate-spec : ∀ a φ → IsSetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) (separate a φ) separate-spec a φ = ℩-spec (hasSeparation a φ) 𝒫 : S → S
The trailing blank line closes this block of operations; the next sections build on them, first deriving intersection without any new axiom.
𝒫 a = ℩ (hasPower a)
Intersection derived from separation
Binary intersection is deliberately not a field. The two-symbol formula var zero ∈̇ con b says "the variable is a member of b"; pass it to separate at a and the axioms return a ∩ b. Its specification is exactly the separation specification, verbatim, because satisfaction of that formula computes to x ∈ˢ b by the defining clauses of ⊨. This is a worked example of the general pattern: whenever a host predicate can be named by a formula, separation turns it into a set.
The definition is one line of applied syntax: a ∩ b separates a along the formula whose only content is the atomic membership statement var zero ∈̇ con b. Because the constant b denotes itself under the interpretation id, satisfying that formula at the environment x ∷ [] reduces, by the defining clauses of satisfaction, to the truth value x ∈ˢ b. The specification theorem is then the separation specification at this particular formula, unchanged: membership in the intersection is the conjunction x ∈ˢ a ⊓ x ∈ˢ b. No new axiom and no new existence proof are spent; a two-symbol formula already names a host predicate that separation can realize.
_∩_ : S → S → S a ∩ b = separate a (var zero ∈̇ con b) ∩-spec : ∀ a b x → (x ∈ˢ (a ∩ b)) ≡ ((x ∈ˢ a) ⊓ (x ∈ˢ b)) ∩-spec a b x = separate-spec a (var zero ∈̇ con b) x
Infinity
One axiom remains, the one that forces a genuinely infinite set into existence. The numerals are the von Neumann naturals: ∅, ∅ ⁺, (∅ ⁺) ⁺, and so on. The record takes the chain itself as a field, pinned down by two propositional equations phrased in raw membership and equality: the zeroth numeral has no members, and the members of a successor numeral are exactly the previous numeral and its members. By extensionality the two equations yield precisely numeral zero ≡ ∅ and numeral (suc n) ≡ numeral n ⁺, so this is exactly as strong as defining the chain outright. What is gained is latitude: the equations never mention the derived ∅, so a concrete model may present the chain in whatever form is most convenient to compute with on its carrier and discharge them without ever unfolding the description operator.
The chain is a function numeral : ℕ → S, so indexing by the host's natural numbers is explicit data. The zero case is a negative condition: any inhabitant z of the Type-valued membership z ∈ˢ numeral zero yields a contradiction, witnessed in the empty host type Empty.⊥. Note the reading: ∈ˢ returns a proposition in hProp ℓ, ⟨_⟩ takes its underlying type, and from an inhabitant of that type the field derives absurdity. This says the zeroth numeral has no members, without mentioning the derived empty set.
field numeral : ℕ → S numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → Empty.⊥ numeral-suc : (n : ℕ) (z : S) → (⟨ z ∈ˢ numeral (suc n) ⟩ → ⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩)
The successor case is a pair of implications, both inside the truncated-free propositional reading. The first says a member z of numeral (suc n) is a member of numeral n or structurally equal to it, the disjunction being the hProp ⊔; the second says every such member of the previous numeral, or thing equal to it, is a member of the successor. Together the two directions say the members of a successor numeral are exactly the previous numeral together with its members, which is exactly the von Neumann step, stated only with ∈ˢ and ≈ˢ.
× (⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩ → ⟨ z ∈ˢ numeral (suc n) ⟩)
isNumeral determines the class of objects equal to some numeral. The quantification runs over ℕ lifted to the working level, since the indexing data lives at the bottom universe. The chosen form of the axiom of infinity says that this exact class is a set. Consequently ω is characterized in both directions: every numeral belongs to it, and every member is equal to a numeral.
The class isNumeral is an existential written directly in hProp: ∃[ x ] P x quantifies over a carrier type and disjoins the family of propositions x ≈ˢ numeral (lower n). The carrier must have type Type ℓ for ∃[ x ] P x to apply, but ℕ lives at Type ℓ-zero; Lift {ℓ-zero} {ℓ} ℕ raises it to the working level, and lower recovers the plain index to feed to numeral. This is a level adjustment, not a mathematical change: the lifted type carries exactly the same elements. The field hasInfinity then asserts, in the now-familiar form, unique existence of a set realizing this class.
isNumeral : S → hProp ℓ isNumeral x = ∃[ n ∶ Lift {ℓ-zero} {ℓ} ℕ ] x ≈ˢ numeral (lower n) field hasInfinity : isContr (SetOf isNumeral) ω : S
As with every other unique existence, ω is the centre extracted by ℩ from hasInfinity. Because the class realized is isNumeral itself, the specification ℩-spec says every member of ω is equal to some numeral; that is what makes this strong form usable as the set of naturals, not merely a set into which the numerals embed.
ω = ℩ hasInfinity
First theorems
Extensionality upgrades the whole existence machinery once and for all: by setOf-unique, whenever a class has a realizer, that realizer is the unique realizer, and the realizer's type is contractible with it as center. Every derived set of this chapter therefore comes with its uniqueness.
ZFC: choice as an extension
The axiom of choice is taken in choice-set form: given a set a whose members are nonempty and pairwise disjoint, some set meets each member of a in exactly one point. This form is stated with membership and the derived intersection alone; its equivalence with the other formulations is model-internal mathematics, deferred until needed. Propositional truncation ∥_∥₁ appears around nonemptiness, the evidence of a shared point, and the existence of a choice set. Thus the axiom asserts existence without selecting witnesses globally. Keeping it as a separate extension rather than a field of the base record preserves the distinction between what ZF proves and what choice adds.
The ZFC record extends rather than repeats: its first field is an entire ZF model, and the line open ... public re-exports all its fields, so anything provable for a ZF model applies verbatim to a ZFC model. Only after this opening does the record declare its own new field, keeping the added axiom cleanly separated from the base theory.
record isZFCModel : Type (ℓ-suc ℓ) where field zf : isZFModel open isZFModel zf public field
The two hypotheses of hasChoice say that a is a family of nonempty, pairwise disjoint sets, each in the reading available here. Nonemptiness is truncated: for each member x of a there merely exists a y in it, ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁, with no chosen witness. Pairwise disjointness is also truncated: if x and y are two members of a that merely share a point z, then x ≡ y holds outright. Note the shape of the disjointness premise: its conclusion is a path in the host, so the truncation of the shared-point evidence is what feeds an untruncated equality.
hasChoice : (a : S) → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁) → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩ → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
The conclusion is likewise a truncated existence: there merely exists a choice set c such that for every member x of a, the intersection c ∩ x has exactly one element, expressed as isContr of the type of its elements. The inner isContr is not a truncation: for each x, it provides an element of c ∩ x and proves that every other such element equals it. The outer truncation applies to the existence of a suitable c, so the axiom supplies no distinguished choice set.
→ ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
Recap
A model of ZF is a record with three kinds of fields: extensionality, which makes realizers unique; unique-existence fields for empty set, pair, union, separation, replacement and power set, with separation and replacement restricted to the book's own formulas; and regularity, stated at the meta level as host well-foundedness of membership, so that recursion and induction along membership are available. ℩ turns fields into operations whose specifications are projections; binary union and successor are composites, and intersection was obtained from separation plus a two-symbol formula whose satisfaction computes directly. Infinity enters as the numeral chain, a function ℕ → S fixed by raw membership equations, and the strong form makes ω a set all of whose members are numerals. isZFCModel adds choice on top, with truncated nonemptiness and shared-point evidence, a truncated conclusion, and an untruncated isContr for each chosen intersection.