Exercise session 7 — Solutions

EXERCISE

Show equivalence bewteen Leibniz equality and eq using eq_rect not rewrite or destruct. You can use refine if it helps.

  Definition eq_to_leib {A} (u v : A) (e : u = v) : u == v :=
    eq_rect _ (fun x => u == x) (refl u) _ e.

  Definition leib_to_eq {A} (u v : A) (e : u == v) : u = v :=
    e (fun x => u = x) eq_refl.

End Leibniz.

Now we're only going to use eq from the standard library.

Similar to eq_rect but for propositions.

About eq_ind.

EXERCISE

Show symmetry, transitivty and congruence (f_equal) for eq, once using eq_ind / eq_rect and once using pattern matching on equality.

Definition eq_sym {A} {u v : A} (e : u = v) : v = u :=
  eq_ind _ (fun x => x = u) eq_refl _ e.

Definition eq_trans {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
  eq_ind _ (fun x => u = x) e _ e'.

Definition eq_sym' {A} {u v : A} (e : u = v) : v = u :=
  match e with
  | eq_refl => eq_refl
  end.

Definition eq_trans' {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
  match e with
  | eq_refl => fun e' => e'
  end e'.

Lemma f_equal' :
  forall A B (f : A -> B) u v, u = v -> f u = f v.
Proof.
  intros A B f u v e.
  destruct e. reflexivity.
Qed.

Definition f_equal_term A B (f : A -> B) u v (e : u = v) : f u = f v :=
  eq_ind _ (fun x => f u = f x) eq_refl _ e.

Definition f_equal_term' A B (f : A -> B) u v (e : u = v) : f u = f v :=
  match e with
  | eq_refl => eq_refl
  end.

EXERCISE

Identify the parameters (uniform and non-uniform) and indices of eq. Then consider the following definition of equality eq_ts with rules for transitivity and symmetry. What are the parameters (unifrom and non-unfirom) and indices? Could the definition be changed (only syntactically) to have more parameters?

Show that eq and eq_ts are equivalent.

Inductive eq_ts {X} : X -> X -> Prop :=
| refl_eq x : eq_ts x x
| sym_eq x y : eq_ts x y -> eq_ts y x
| trans_eq x y z : eq_ts x y -> eq_ts y z -> eq_ts x z.

In eq A u v, A and u are uniform parameters, while v is an index.

For eq_ts A u v, u is also an idex because of the symmetry rule. It could be turned into a non-uniform parameter by changing the symmetry constructor to sym_eq x y : eq_ts y x -> eq_ts x y.

Lemma eq_to_ts A (u v : A) :
  u = v ->
  eq_ts u v.
Proof.
  intros e. subst. apply refl_eq.
Qed.

Lemma eq_from_ts A (u v : A) :
  eq_ts u v ->
  u = v.
Proof.
  intros e.
  induction e.
  - reflexivity.
  - symmetry. assumption.
  - transitivity y. all: assumption.
Qed.

EXERCISE

Show a lemma similar to f_equal but for dependent functions, ie functions of type forall (x : A), B x.

Hint: You can for instance use eq_rect to state the lemma.

Lemma dep_f_equal :
  forall A B (f : forall (x : A), B x) u v (e : u = v),
    eq_rect _ B (f u) _ e = f v.
Proof.
  intros A B f u v e.
  destruct e.
  simpl.
  reflexivity.
Qed.

EXERCISE

Define the inductive predicate for even natural numbers we already saw several times (try to do it without having to look it up).

Then prove that even (S (S n)) implies even n. Try to do it both using tactics (for instance using the remember tactic, but ideally without using inversion directly on even) and by writing a proof term directly.

Do the same to prove that even 1 is false.

Finally, show that n cannot be even at the same time as S n. (This time you can just do it using tactics.)

Inductive even : nat -> Prop :=
| even0 : even 0
| evenS : forall n, even n -> even (S (S n)).

Lemma evenSS_inv n :
  even (S (S n)) ->
  even n.
Proof.
  intros h.
  remember (S (S n)) as m eqn: e.
  destruct h.
  - discriminate.
  - inversion e. subst. assumption.
Qed.

Definition evenSS_inv_alt n (h : even (S (S n))) : even n :=
  match h in even m return m = S (S n) -> even n
  with
  | even0 =>
    fun (e : 0 = S (S n)) =>
      eq_ind 0 (fun x => match x with 0 => True | _ => even n end) I _ e
  | evenS m h' =>
    fun (e : S (S m) = S (S n)) =>
      eq_ind _ even h' _ (f_equal (fun x => pred (pred x)) e)
  end eq_refl.

Lemma not_even1 : ~ even 1.
Proof.
  intro h.
  remember 1 as n eqn: e.
  destruct h.
  - discriminate.
  - discriminate.
Qed.

Definition not_even1_term (h : even 1) : False :=
  match h in even n return n = 1 -> False
  with
  | even0 =>
    fun (e : 0 = 1) =>
      eq_ind 0 (fun x => match x with 0 => True | _ => False end) I _ e
  | evenS m h' =>
    fun (e : S (S m) = 1) =>
      eq_ind (S (S m)) (fun x => match x with S (S n) => True | _ => False end) I _ e
  end eq_refl.

Lemma even_and_S_False n :
  even n ->
  even (S n) ->
  False.
Proof.
  intros hn hSn.
  induction hn as [| n hn ih] in hSn |- *.
  - apply not_even1. assumption.
  - apply ih. apply evenSS_inv. assumption.
Qed.

EXERCISE

Define the map function on lists.

Show that map (fun x => x) l is the same as l. Can you prove that map (fun x => x) is equal to the identity function?

Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: l' => f x :: map f l'
  end.

Lemma map_id A (l : list A) :
  map (fun x => x) l = l.
Proof.
  induction l.
  - reflexivity.
  - simpl. f_equal. assumption.
Qed.

We cannot prove that it's the identity function without function extensionality.

Equality principles

EXERCISE

We give some equality principles below. You may assume some of them when solving the exercises below. Try to assume only what you need.

Show that map (fun x => x) is equal to the identity function.

Show that inhabited propositions are equal to True. Similarly, show that uninhabited propositions are equal to False.

Show that two predicates are equal as soon as they are logically equivalent: ie. as soon as forall x, P x <-> Q x.

Show that proof irrelevance follows from proposition extensionality.

Show that UIP follows from proof irrelevance.

Show that UIP and K are equivalent.

Definition FunExt :=
  forall A B (f g : A -> B), (forall x, f x = g x) -> f = g.

Definition PropExt :=
  forall (P Q : Prop), (P <-> Q) -> P = Q.

Definition ProofIrrelevance :=
  forall (P : Prop) (p q : P), p = q.

Definition UIP :=
  forall A (u v : A) (p q : u = v), p = q.

Definition K :=
  forall A (u : A) (e : u = u), e = eq_refl.

Axiom funext : FunExt.

Lemma map_id' A :
  map (fun (x : A) => x) = (fun l => l).
Proof.
  apply funext.
  apply map_id.
Qed.

Axiom propext : PropExt.

Lemma inhabited_is_True (P : Prop) :
  P ->
  P = True.
Proof.
  intros h.
  apply propext. split.
  - intro. constructor.
  - intro. assumption.
Qed.

Lemma neg_eq_False (P : Prop) :
  ~ P -> P = False.
Proof.
  intros h.
  apply propext. split.
  - assumption.
  - intro bot. destruct bot.
Qed.

Lemma predext A (P Q : A -> Prop) :
  (forall x, P x <-> Q x) ->
  P = Q.
Proof.
  intros h.
  apply funext. intro x.
  apply propext. apply h.
Qed.

Lemma proof_irrelevance :
  (* using PropExt axiom *)
  ProofIrrelevance.
Proof.
  intros P p q.
  pose proof (inhabited_is_True P p).
  subst. destruct p, q.
  reflexivity.
Qed.
Print Assumptions proof_irrelevance.

Definition PI_UIP : ProofIrrelevance -> UIP.
Proof.
  intros pi A u v p q.
  apply pi.
Qed.

Definition UIP_K : UIP -> K.
Proof.
  intros uip A u e.
  apply uip.
Qed.

Definition K_UIP : K -> UIP.
Proof.
  intros k A u v p q.
  destruct q. apply k.
Qed.

EXERCISE

Define Boolean equality for natural numbers, i.e. some eq_nat : nat -> nat -> bool. (You may have already done it, but try to do it again.)

Show that when eq_nat n m is true, then n = m. Show that when it is false, then n <> m.

Deduce that equality of natural numbers is decidable. This is typically achieved by defining eq_dec : forall n m, { n = m } + { n <> m }. You can first do it with tactics but try to do it with a proof term.

To know more about the {} + {} type, execute the following commands. Locate can tell you what is the name of an object or notation. Print for an inductive will tell you the name and type of its constructors.

Locate "{ _ } + { _ }".
Print sumbool.

Fixpoint eq_nat (n m : nat) : bool :=
  match n, m with
  | 0, 0 => true
  | S n, S m => eq_nat n m
  | _, _ => false
  end.

Lemma eq_nat_eq n m :
  eq_nat n m = true -> n = m.
Proof.
  induction n in m |- *.
  - destruct m. 2: discriminate.
    reflexivity.
  - destruct m. 1: discriminate.
    intro e. f_equal. apply IHn. assumption.
Qed.

Lemma eq_eq_nat n m :
  n = m -> eq_nat n m = true.
Proof.
  induction n in m |- *.
  - destruct m. 2: discriminate.
    reflexivity.
  - destruct m. 1: discriminate.
    intro e. simpl. apply IHn.
    inversion e. reflexivity.
Qed.

Lemma eq_dec (n m : nat) :
  { n = m } + { n <> m }.
Proof.
  destruct (eq_nat n m) eqn: e.
  - left. apply eq_nat_eq. assumption.
  - right. intro e'. apply eq_eq_nat in e'.
    rewrite e' in e. discriminate.
Qed.

Lemma eq_nat_false n m :
  eq_nat n m = false -> n <> m.
Proof.
  intros e. intro e'.
  apply eq_eq_nat in e'. congruence.
Qed.

Definition eq_dec_term (n m : nat) : { n = m } + { n <> m } :=
  match eq_nat n m as b return eq_nat n m = b -> { n = m } + { n <> m } with
  | true => fun (e : eq_nat n m = true) => left (eq_nat_eq n m e)
  | false => fun (e : eq_nat n m = false) => right (eq_nat_false n m e)
  end eq_refl.

EXERCISE

Show extensionality for subset types. In other words to prove that exist _ x hx = exist _ y hy, it is enough to show x = y.

Hint: You may require an axiom to do it. It's fine to assume it and keep going.

Lemma sig_ext A (P : A -> Prop) x y hx hy :
  x = y ->
  exist _ x hx = exist _ y hy :> { x | P x }.
Proof.
  intros e.
  destruct e. f_equal.
  apply proof_irrelevance.
Qed.

Equivalence

There are many ways to define equivalence in Rocq. We will choose one using some notion of unique existence, defined below.

We will say that a function is an equivalence when there exists a unique antecedent to each point.

Print unique.

Notation "{ ! x | P }" := (sig (unique (fun x => P))) : type_scope.
Notation "{ ! x : A | P }" := (sig (A := A) (unique (fun x => P))) : type_scope.

Definition isEquiv {X Y} (f : X -> Y) :=
  forall y, { ! x | y = f x }.

Definition equivalence X Y :=
  { f : X -> Y & isEquiv f }.

EXERCISE

Show that equivalences form an equivalence relation, that is that they are reflexive, symmetric and transitive.

Next, show that nat is equivalent to nat*, ie nonzero natural numbers. Hint: You can define this as a subset type (using {}) of nat. Hint: You may need one extra axiom to complete the proof.

Lemma equivalence_refl X : equivalence X X.
Proof.
  exists (fun x => x).
  intro y. exists y. split.
  - reflexivity.
  - intros x e. assumption.
Defined.

Lemma equivalence_sym X Y :
  equivalence X Y ->
  equivalence Y X.
Proof.
  intros [f h].
  unshelve eexists.
  - intro y. specialize (h y). destruct h as [x h]. exact x.
  - intro x. exists (f x). split.
    + destruct (h (f x)) as [x' [e h']]. simpl.
      symmetry. apply h'. reflexivity.
    + intros y e.
      destruct (h y) as [x' [e' h']]. simpl in e.
      subst. reflexivity.
Defined.

Lemma equivalence_trans X Y Z :
  equivalence X Y ->
  equivalence Y Z ->
  equivalence X Z.
Proof.
  intros [f hf] [g hg].
  exists (fun x => g (f x)).
  intro z. specialize (hg z) as [y [e hy]]. subst.
  specialize (hf y) as [x [e hx]]. subst.
  exists x. split.
  - reflexivity.
  - intros w e. apply hy in e. apply hx in e. assumption.
Qed.

Definition natNZ := { n : nat | n <> 0 }.

Lemma equiv_nat_natNZ :
  equivalence nat natNZ.
Proof.
  assert (hdiscr : forall n, S n <> 0).
  { discriminate. }
  unshelve eexists.
  { intros n. exists (S n). apply hdiscr. }
  intros [n hn].
  exists (pred n). split.
  - apply sig_ext. lia.
  - intros m hm. inversion hm. lia.
Qed.

EXERCISE

Define a predicate on types that says that a type has exactly one inhabitant.

Deduce that unit is different from bool.

Next, show that nat is different from bool.

Definition all_equal A := forall (x y : A), x = y.

Lemma unit_neq_bool :
  unit <> bool.
Proof.
  intro e.
  assert (h : all_equal unit).
  { intros [] []. reflexivity. }
  rewrite e in h.
  specialize (h true false). discriminate.
Qed.

Lemma nat_bool :
  nat <> bool.
Proof.
  pose (p X := forall x y z : X, x = y \/ x = z \/ y = z).
  assert (h : p bool).
  { intros [] [] []. all: tauto. }
  intros E. rewrite <- E in h.
  specialize (h 0 1 2). lia.
Qed.

EXERCISE

Until now, the equalities we considred have been homogenous, meaning u = v requires both u and v to have the same type. You even have a notation to give the common type u = v :> A.

In some cases, it makes sense to compare two objects of a priori different types. We can say that u : A and v : B are heterogenously equal when, first A = B and then u = v up to a transport from A to B.

We can also define it inductively. Show that the two versions are equivalent.

Definition cast {A B} (e : A = B) (t : A) : B :=
  match e with
  | eq_refl => t
  end.

Definition heq {A B} (u : A) (v : B) :=
  { e : A = B & cast e u = v }.

Inductive Heq {A} (u : A) : forall {B}, B -> Prop :=
| heq_refl : Heq u u.

Lemma heq_Heq A B (u : A) (v : B) :
  heq u v -> Heq u v.
Proof.
  intros [e h].
  destruct e. cbn in h. subst.
  constructor.
Qed.

Lemma Heq_heq A B (u : A) (v : B) :
  Heq u v -> heq u v.
Proof.
  intros e.
  destruct e.
  exists eq_refl. cbn. reflexivity.
Qed.

EXERCISE

Does heterogneous equality imply homogenous equality? In other words can you prove the following? forall A (u v : A), Heq u v -> u = v

Hint: Maybe it requires an axiom?

Lemma heq_to_eq A (u v : A) :
  K ->
  Heq u v ->
  u = v.
Proof.
  intros k h.
  apply Heq_heq in h. destruct h as [p q].
  assert (p = eq_refl).
  { apply k. }
  subst.
  reflexivity.
Qed.

EXERCISE

Show that nat is equivalent to even natural numbers.

Lemma even_double n :
  even (n * 2).
Proof.
  induction n.
  - constructor.
  - simpl. constructor. assumption.
Qed.

Fixpoint div2 (n : nat) : nat :=
  match n with
  | 0 => 0
  | 1 => 0
  | S (S n) => S (div2 n)
  end.

Lemma double_div2 n :
  even n ->
  div2 n * 2 = n.
Proof.
  intros h.
  induction h.
  - reflexivity.
  - simpl. f_equal. f_equal. assumption.
Qed.

Lemma div2_double n :
  div2 (n * 2) = n.
Proof.
  induction n.
  - reflexivity.
  - simpl. f_equal. assumption.
Qed.

Lemma equivalence_nat_even :
  equivalence nat { n : nat | even n }.
Proof.
  unshelve eexists (fun n => exist _ (n * 2) _).
  { simpl. apply even_double. }
  intros [n h]. exists (div2 n). split.
  - apply sig_ext. rewrite double_div2. 2: assumption.
    reflexivity.
  - intros m e. inversion e.
    apply div2_double.
Qed.

EXERCISE

Prove Cantor's theorem for bool: Show that there are no surjections from X to X -> bool. In other words there are no f : X -> (X -> bool) such that for all p there exists x such that f x = p.

Prove Cantor's theorem: Show that there are no surjections from X to X -> Prop.

Theorem Cantor_bool X :
  ~ exists (f : X -> (X -> bool)), forall p, exists x, f x = p.
Proof.
  intros [f Hf].
  destruct (Hf (fun x => negb (f x x))) as [x Hx].
  enough (f x x = negb ( f x x)).
  { destruct (f x x); simpl in *; discriminate. }
  apply (f_equal (fun g => g x)) in Hx.
  now rewrite <- Hx.
Qed.

Theorem Cantor X :
  ~ exists f : X -> (X -> Prop), forall p, exists x, f x = p.
Proof.
  intros [f Hf].
  destruct (Hf (fun x => ~ f x x)) as [x Hx].
  enough (f x x <-> ~ f x x) by tauto.
  apply (f_equal (fun g => g x)) in Hx.
  now rewrite <- Hx.
Qed.

(*
^^^^^^^^
EXERCISE
^^^^^^^^

Now prove the following theorem:
*)

Theorem Lawvere X Y :
  forall (f : X -> (X -> Y)),
    (forall g, exists x, f x = g) ->
    forall (g : Y -> Y), exists y, g y = y.
Proof.
  intros f Hf g.
  destruct (Hf (fun x => g (f x x))) as [x Hx].
  exists (f x x).
  apply (f_equal (fun g => g x)) in Hx.
  now rewrite <- Hx.
Qed.

EXERCISE

Can you get a simpler proof of the Cantor theorem for bool now?

Theorem Cantor_bool' X :
  ~ exists f : X -> (X -> bool), forall p, exists x, f x = p.
Proof.
  intros [f Hf].
  apply Lawvere with (g := negb) in Hf as [y Hy].
  destruct y; simpl in Hy; discriminate.
Qed.

J eliminator

We have seen eq_rect / eq_ind, but equality actually enjoys a stronger induction principle called the J eliminator. Instead of considering a predicate on an element, we also consider that the predicate depends on an equality and that we only need to show it when the equality is reflexivity to get it for all equalities.

Its type is the following. Show that you can indeed derive it.

Definition J :
  forall {A} {u : A} (P : forall z, u = z -> Prop) {v : A} (t : P u eq_refl) (e : u = v),
    P v e.
Proof.
  intros A u P v t e.
  destruct e. assumption.
Defined.

EXERCISE

We are now going to show that J is equivalent to singletons being contractible, ie that singletons have a exactly one element. For this we are going back to the world of Leibniz equality which does not enjoy J.

You have to fill a few ``REPLACE_ME``s but you should have solved them already so you can easily copy paste your definitions.

You can then prove the equivalence at the end of the module Leibniz2.

Module Leibniz2.

  Definition leib_eq {A} (u v : A) :=
    forall (P : A -> Prop), P u -> P v.

  Notation "u == v" := (leib_eq u v) (at level 80).

  Definition refl {A} (a : A) : a == a :=
    fun P (h : P a) => h.

  Definition sym {A} (u v : A) (e : u == v) : v == u :=
    fun P => e (fun x => P x -> P u) (refl u P).

  Lemma trans {A} (u v w : A) (e : u == v) (e' : v == w) : u == w.
  Proof.
    intro P.
    apply e'. apply e.
  Defined.

  Definition J_prop :=
    forall A (u : A) (P : forall z, u == z -> Prop) v (t : P u (refl u)) (e : u == v),
      P v e.

  Definition singleton {A} (x : A) := { y | x == y }.

  Definition incl {A} (x : A) : singleton x :=
    exist _ x (refl x).

  Definition all_equal (A : Type) :=
    forall (x y : A), x == y.

  Lemma all_equal_implies_J :
    (forall A (x : A), all_equal (singleton x)) ->
    J_prop.
  Proof.
    intro h. intros A u P v t e.
    specialize (h _ u). specialize (h (incl u) (exist _ v e)).
    specialize (h (fun '(exist _ x e) => P x e)).
    simpl in h. apply h. assumption.
  Qed.

  Lemma all_equal_incl :
    forall A (x : A),
      (forall u, incl x == u) ->
      all_equal (singleton x).
  Proof.
    intros A x h. intros u v.
    eapply trans.
    - apply sym. apply h.
    - apply h.
  Qed.

  Lemma J_implies_all_equal :
    J_prop ->
    (forall A (x : A), all_equal (singleton x)).
  Proof.
    intros J. intros A x.
    apply all_equal_incl. intro u. intros P h.
    destruct u as [y e].
    specialize (J _ x (fun m p => P (exist _ m p))).
    apply J. assumption.
  Qed.

End Leibniz2.

EXERCISE

Uniqueness of identity proofs (UIP) is not provable in general but it still holds for specific types, namely types with a decidable equality. This fact is known as Hedberg's theorem.

We thus state UIP_for, so that UIP_for X means UIP holds for type X.

We're going first to prove UIP holds for nat.

Definition UIP_for X :=
  forall (u v : X) (p q : u = v), p = q.

Lemma nat_eqdec_eq x :
  PeanoNat.Nat.eq_dec x x = left eq_refl.
Proof.
  induction x.
  - reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

Lemma UIP_nat' (x y: nat) :
  forall (e : x = y),
    match PeanoNat.Nat.eq_dec x y with
    | left e' => eq_ind _ _ eq_refl _ e' = e
    | _ => True
    end.
Proof.
  destruct e. rewrite nat_eqdec_eq. reflexivity.
Qed.

Fact UIP_refl_nat (x: nat) :
  forall (e : x = x), e = eq_refl.
Proof.
  intros e.
    generalize (UIP_nat' x x e).
    rewrite nat_eqdec_eq. cbv. intros []. reflexivity.
Qed.

Lemma UIP_for_nat : UIP_for nat.
Proof.
  intros u v p q.
  destruct q. apply UIP_refl_nat.
Qed.

EXERCISE

We are now going to prove the general case. Prove Hedberg's theorem as follows.

Definition HF X (f : forall (x y : X), x = y -> x = y) :=
  forall x y (e e' : x = y), f x y e = f x y e'.

Lemma Hedberg' X :
  ex (HF X) -> UIP_for X.
Proof.
  intros [f H] x y.
  enough (forall e: x = y,  eq_trans (f x y e) (eq_sym (f y y eq_refl)) = e) as H1.
  - intros e e'. specialize (H _ _ e e'). congruence.
  - destruct e. cbv. destruct f; reflexivity.
Qed.

Theorem Hedberg X :
  (forall x y: X, x = y \/ x <> y) -> UIP_for X.
Proof.
  intros d. apply Hedberg'.
  exists (fun x y e => match d x y with or_introl e' => e' | _ => e end).
  intros x y e e'.
  destruct d as [e''|h].
  - reflexivity.
  - exfalso. exact (h e).
Qed.

EXERCISE

Using FunExt, we can show that two functions of type nat -> bool are equal if and only if they are not not equal. Prove it.

Definition stable (P : Prop) :=
  ~~P -> P.

Fact FE_stable_HF X :
  FunExt ->
  (forall (x y : X), stable (x = y)) ->
  sig (HF X).
Proof.
  intros F G.
  exists (fun x y e => G x y (fun f => match f e with end)).
  intros x y e e'. f_equal. apply F. intros f.
  exfalso. exact (f e).
Qed.

Fact FE_test_eq_stable :
  FunExt ->
  forall (f g : nat -> bool), stable (f = g).
Proof.
  intros F f g H. apply F. intros x.
  destruct (f x) eqn:E1, (g x) eqn:E2.
  - reflexivity.
  - contradict H. intros ->. contradict E1. rewrite E2. discriminate.
  - contradict H. intros ->. contradict E1. rewrite E2. discriminate.
  - reflexivity.
Qed.

EXERCISE

You may or may not have heard of homotopy type theory (HoTT) and univalent foundations. This is a relatively recent development in which equality of types corresponds to equivalences. This essentially justifies the informal mathematical practice of considering isomorphic objects to be the same.

Define a term to_equiv that inhabits equivalence X Y from X = Y.

Univalence is then stated as this function being itself being an equivalence.

Definition to_equiv X Y : X = Y -> equivalence X Y.
Proof.
  intro e. destruct e. apply equivalence_refl.
Defined.

Definition Univalence :=
  forall (X Y : Type), isEquiv (to_equiv X Y).

EXERCISE

Show that assuming univalence, equivalent types are equal.

Lemma univalence_equiv_equal :
  Univalence ->
  (forall X Y, equivalence X Y -> X = Y).
Proof.
  intros uni X Y h.
  assert (h' : equivalence (X = Y) (equivalence X Y)).
  { exists (to_equiv X Y). apply uni. }
  apply equivalence_sym in h'.
  destruct h' as [f h'].
  apply f. assumption.
Qed.

EXERCISE

Univalence is incompatible with UIP. One way is to show that equivalence A B = (A = B) and that there are two equivalences between bool and itself, thus negating UIP.

Definition equivalence_neg_bool : equivalence bool bool.
Proof.
  exists negb.
  intro b. exists (negb b). split.
  - destruct b. all: reflexivity.
  - intros b' e. destruct b, b'. all: try discriminate. all: reflexivity.
Defined.

Lemma equivalence_eq_eq :
  forall A B,
    Univalence ->
    equivalence A B = (A = B).
Proof.
  intros A B uni.
  symmetry. apply univalence_equiv_equal. 1: assumption.
  exists (to_equiv A B).
  apply uni.
Qed.

Lemma Univalence_neg_UIP :
  Univalence -> ~ UIP.
Proof.
  intros uni uip.
  pose proof (equivalence_eq_eq bool bool uni) as e.
  assert (h : forall p q : equivalence bool bool, p = q).
  { rewrite e. intros. apply uip. }
  specialize (h (equivalence_refl bool) equivalence_neg_bool).
  inversion h.
  apply (f_equal (fun x => x true)) in H0.
  simpl in H0. discriminate.
Qed.