gistfile1.txt

Theorem axiom-of-choice : [
  {A : U{i}} {B : A -> U{i}} {Q : (a : A) B a -> U{i}}
    (q : (a : A) ((b : B a) * Q a b)) -> (f : (a : A) B a) * ((a : A) Q a (f a))
] {
  auto;
  intro [lam(x. spread(q x; a.b.a))]; auto;
  reduce;
  elim <q> [a]; auto;
  hyp-subst <- #7 [h. Q a spread(h; a._.a)]; auto;
  elim <y>; reduce; assumption
}.


Theorem polymorphic-id-unique : [
  {f : {A : U{i}} A -> A} =(f; id; {A : U{i}} A -> A)
] {
  auto;
  ext; unfold <id>; auto;
  aux {
    elim <f> [A]; auto;
    hyp-subst <- #4 [h.=(h; h; _)]; auto
  };

  reduce;
  elim <f> [{b : A | =(b; x; A)}];
  auto;

  hyp-subst <- #5 [h. =(h _; _; _)];
  aux {
    auto;
    elim <h> [x]; auto;
    hyp-subst <- #8 [z. =(z; z; _)]; auto
  };

  elim #4 [x]; auto;
  hyp-subst <- #7 [h. =(h; _; _)]; auto;
  elim #6;
  assumption
}.

Print polymorphic-id-unique.