# Universes

In what follows, we will work with explicit universes rather than with Coq-style implicit universes.
For that, we define two universes Typ1 and Typ2 as shorthands for the generic universe Type by enforcing the constraint Typ1 : Typ2 so that Coq knows that the implicit index associated to Typ1 is smaller than the implicit index associated to Typ2.

Definition Typ2 := Type.
Definition Typ1 : Typ2 := Type.
Intuitively:
• Typ1 is the universe of small types, which contains the type Prop of propositions, and is closed under dependent product.
• Typ2 is the top-universe of large types, which contains the universe Typ1, and is closed under dependent product again.
In the following, small types (i.e. the inhabitants of Typ1) will be used as the carriers of pointed graphs (for representing sets).
The type of binary relations:

Definition Rel (X : Typ1) : Typ1 := X X Prop.

# Logical connectives

To avoid the use of Coq-style inductive definitions, we redefine all the logical connectives from their second-order encoding and give their introduction rules. Except in a few cases, it is not necessary to give the corresponding elimination rules whose behaviour is mimicked by using the tactic Apply H (instead of Elim H) in the subsequent proof-scripts.

## Truth and falsity

Definition top : Prop := E : Prop, E E.

Lemma top_intro : top.
Proof fun E ee.

Definition bot : Prop := E : Prop, E.

## Conjunction

Definition and (A B : Prop) : Prop := E : Prop, (A B E) E.

Lemma and_intro : A B : Prop, A B and A B.
Proof fun A B a b E ff a b.

Lemma and_fst : A B : Prop, and A B A.
Proof fun A B pp A (fun a _a).

Lemma and_snd : A B : Prop, and A B B.
Proof fun A B pp B (fun _ bb).

## Disjunction

Definition or (A B : Prop) : Prop :=
E : Prop, (A E) (B E) E.

Lemma or_inl : A B : Prop, A or A B.
Proof fun A B a E f gf a.

Lemma or_inr : A B : Prop, B or A B.
Proof fun A B b E f gg b.

## Logical equivalence

Definition iff (A B : Prop) : Prop := and (A B) (B A).

# Existential quantifiers and Leibniz equality

## Existential quantification in a given small type

Definition ex (X : Typ1) (P : X Prop) : Prop :=
E : Prop, ( x : X, P x E) E.

Lemma ex_intro : (X : Typ1) (P : X Prop) (x : X), P x ex X P.
Proof fun X P x p E ff x p.

We define a variant of the former existential quantification in order to express the existence of an object that fulfills the conjunction of two predicates P and Q.

Definition ex2 (X : Typ1) (P Q : X Prop) : Prop :=
E : Prop, ( x : X, P x Q x E) E.

Lemma ex2_intro :
(X : Typ1) (P Q : X Prop) (x : X), P x Q x ex2 X P Q.
Proof fun X P Q x p q E ff x p q.

## Existential quantification over all small types

Definition exT (P : Typ1 Prop) : Prop :=
E : Prop, ( X : Typ1, P X E) E.

Lemma exT_intro : (P : Typ1 Prop) (X : Typ1), P X exT P.
Proof fun P X p E ff X p.

## Existential quantification over all pointed graphs

Definition exG (P : X : Typ1, Rel X X Prop) : Prop :=
E : Prop, ( (X : Typ1) (A : Rel X) (a : X), P X A a E) E.

Lemma exG_intro :
(P : X : Typ1, Rel X X Prop) (X : Typ1)
(A : Rel X) (a : X), P X A a exG P.

Proof fun P X A a p E ff X A a p.

## Leibniz equality

Definition eq (X : Typ1) (x y : X) : Prop := P : X Prop, P x P y.

Lemma eq_refl : (X : Typ1) (x : X), eq X x x.
Proof fun X x P pp.

Lemma eq_sym : (X : Typ1) (x y : X), eq X x y eq X y x.
Proof fun X x y ee (fun zeq X z x) (eq_refl X x).

Lemma eq_trans :
(X : Typ1) (x y z : X), eq X x y eq X y z eq X x z.
Proof fun X x y z e1 e2 P pe2 P (e1 P p).

# Some data structures

## Option type

The option type (opt X) : Typ1 (parametrized by X : Typ1) that would be inductively defined in Coq by
Inductive opt : Typ1 := | some : X->(opt X) | none : (opt X).
is mimicked by the following definitions:

Definition opt (X : Typ1) : Typ1 := (X Prop) Prop.
Definition some (X : Typ1) (x : X) : opt X := fun ff x.
Definition none (X : Typ1) : opt X := fun _bot.

These definitions fulfill the expected properties of injectivity and non-confusion:

Lemma eq_some_some :
(X : Typ1) (x1 x2 : X),
eq (opt X) (some X x1) (some X x2) eq X x1 x2.

Proof fun X x1 x2 ee (fun zz (fun xeq X x1 x)) (eq_refl X x1).

Lemma eq_some_none :
(X : Typ1) (x : X), eq (opt X) (some X x) (none X) bot.

Proof fun X x ee (fun zz (fun _top)) top_intro.

Lemma eq_none_some :
(X : Typ1) (x : X), eq (opt X) (none X) (some X x) bot.

Proof
fun X x ee (fun zz (fun _top) bot) (fun pp) top_intro.

On the other hand, the corresponding elimination scheme does not hold, due to the existence of inhabitants of the type (opt X) that are neither of the form (some X x) nor of the form (none X), such as the term f:XProptop : (opt X) for instance.
In practice, the existence of such parasitic elements will not pose a problem. When defining edge relations on data-types such as (opt X), we will simply ignore these extra elements so that they will become invisible up to a bisimulation.

## Extended sum type

The (extended) sum type (sum X Y) : Typ1 (parametrized by the types X,Y : Typ1) that would be inductively defined in Coq by
Inductive sum X,Y:Typ1 : Typ1 := | inl : X->(sum X Y) (left injection) | inr : Y->(sum X Y) (right injection) | out : (sum X Y). (extra element)
is mimicked by the following definitions:

Definition sum (X Y : Typ1) : Typ1 := (X Prop) (Y Prop) Prop.
Definition inl (X Y : Typ1) (x : X) : sum X Y := fun f _f x.
Definition inr (X Y : Typ1) (y : Y) : sum X Y := fun _ gg y.
Definition out (X Y : Typ1) : sum X Y := fun _ _bot.

Again, these definitions fulfill the expected properties of injectivity and non-confusion:

Lemma eq_inl_inl :
(X Y : Typ1) (x1 x2 : X),
eq (sum X Y) (inl X Y x1) (inl X Y x2) eq X x1 x2.

Proof
fun X Y x1 x2 e
e (fun zz (fun xeq X x1 x) (fun _bot)) (eq_refl X x1).

Lemma eq_inr_inr :
(X Y : Typ1) (y1 y2 : Y),
eq (sum X Y) (inr X Y y1) (inr X Y y2) eq Y y1 y2.

Proof
fun X Y y1 y2 e
e (fun zz (fun _bot) (fun yeq Y y1 y)) (eq_refl Y y1).

Lemma eq_inl_inr :
(X Y : Typ1) (x : X) (y : Y),
eq (sum X Y) (inl X Y x) (inr X Y y) bot.

Proof fun X Y x y ee (fun zz (fun _top) (fun _bot)) top_intro.

Lemma eq_inr_inl :
(X Y : Typ1) (x : X) (y : Y),
eq (sum X Y) (inr X Y y) (inl X Y x) bot.

Proof fun X Y x y ee (fun zz (fun _bot) (fun _top)) top_intro.

Lemma eq_inl_out :
(X Y : Typ1) (x : X), eq (sum X Y) (inl X Y x) (out X Y) bot.

Proof fun X Y x ee (fun zz (fun _top) (fun _top)) top_intro.

Lemma eq_out_inl :
(X Y : Typ1) (x : X), eq (sum X Y) (out X Y) (inl X Y x) bot.

Proof
fun X Y x e
e (fun zz (fun _top) (fun _top) bot) (fun pp) top_intro.

Lemma eq_inr_out :
(X Y : Typ1) (y : Y), eq (sum X Y) (inr X Y y) (out X Y) bot.

Proof fun X Y y ee (fun zz (fun _top) (fun _top)) top_intro.

Lemma eq_out_inr :
(X Y : Typ1) (y : Y), eq (sum X Y) (out X Y) (inr X Y y) bot.

Proof
fun X Y y e
e (fun zz (fun _top) (fun _top) bot) (fun pp) top_intro.

The corresponding elimination scheme does not hold here, for the same reason as for the option type (see above).