Transcription of http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html into Coq

UnivalenceFromScratch.v

(* -*- coq-prog-args: ("-indices-matter") -*- *)
(** Initial setup stuff to print sigma types with projections rather than as matches *)
Set Primitive Projections.
Set Universe Polymorphism.
Record sigT {A:Type} (P:A -> Type) : Type :=
  existT { pr1 : A ; pr2 : P pr1 }.
Arguments sigT (A P)%type.
Arguments pr1 {A P} _.
Arguments pr2 {A P} _.
Arguments existT {_} _ _ _.
Notation "{ x : A  & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "( x ; y )" := (existT _ x y).
(** Transcription begins here *)

Inductive Id {X} : X -> X -> Type
  := refl (x : X) : Id x x.

Definition J {X}
           (A : forall x y, Id x y -> Type)
           (f : forall x, A x x (refl x))
           (x y : X) (p : Id x y)
  : A x y p
  := match p return A _ _ p with
     | refl x => f x
     end.

Definition isSingleton : Type -> Type
  := fun X => { c : X & forall x, Id c x }.

Definition fiber {X Y} : (X -> Y) -> Y -> Type
  := fun f y => { x : _ & Id (f x) y }.

Definition isEquiv {X Y} : (X -> Y) -> Type
  := fun f => forall y, isSingleton(fiber f y).

Definition Eq : Type -> Type -> Type
  := fun X Y => { f : X -> Y & isEquiv f }.

Definition singletonType {X} : X -> Type
  := fun x => { y : _ & Id y x }.

Definition η {X} (x : X) : singletonType x
  := (x; refl x).

Definition singletonTypesAreSingletons {X} (x : X) : isSingleton(singletonType x)
  := let A : forall y x : X, Id y x -> Type
         := fun y x p => Id (η x) (y ; p) in
     let f : forall (x : X), A x x (refl x)
         := fun x => refl (η x) in
     let φ : forall (y x : X) (p : Id y x), Id (η x) (y ; p)
         := J A f in
     let g : forall (x : X) (σ : singletonType x), Id (η x) σ
         := fun x '(y ; p) => φ y x p in
     let h : forall (x : X), { c : singletonType x & forall (σ : singletonType x), Id c σ }
         := fun x => (η x ; g x) in
     h x.

Definition id X : X -> X
  := fun x => x.

Definition idIsEquiv X : isEquiv(id X)
  := let g : forall (x : X), isSingleton (fiber (id X) x)
         := singletonTypesAreSingletons in
     g.

Definition IdToEq : forall X Y, Id X Y -> Eq X Y
  := let A : forall X Y, Id X Y -> Type
         := fun X Y p => Eq X Y in
     let f : forall X, A X X (refl X)
         := fun X => (id X ; idIsEquiv X) in
     J A f.

Definition isUnivalentAt (X Y : Type) : Type
  := isEquiv(IdToEq X Y).
Definition isUnivalent@{U U'} : Type@{U'}
  := forall (X Y : Type@{U}), isUnivalentAt@{U U U' U' U} X Y.

Opaque J.
Set Printing Universes.
Monomorphic Universes U U'.
Module Short.
  Notation "'λ' x → f" := (fun x => f) (at level 200, right associativity) : core_scope.
  Notation "'λ' x → f" := (fun x => f) (at level 200, right associativity) : type_scope.
  Notation "( x  :  T )  →  f" := (forall x : T, f) (at level 200, right associativity) : type_scope.
  Notation Σ f := (@sigT _ f).
  Set Printing Width 500.
  Eval compute in isUnivalent@{U U'}.
(** = (X : Type@{U}) → (Y : Type@{U}) → (y : Σ (λ f → (y : Y) → Σ (λ c
     → (x : Σ (λ x → Id@{U} (f x) y)) → Id@{U} c x))) → Σ (λ c → (x :
     Σ (λ x → Id@{U} (J@{U U'} (λ X0 → λ Y0 → λ _ → Σ (λ f → (y0 : Y0)
     → Σ (λ c0 → (x0 : Σ (λ x0 → Id@{U} (f x0) y0)) → Id@{U} c0 x0)))
     (λ X0 → (λ x0 → x0; λ x0 → ((x0; refl@{U} x0); λ pat → J@{U U} (λ
     y0 → λ x1 → λ p → Id@{U} (x1; refl@{U} x1) (y0; p)) (λ x1 →
     refl@{U} (x1; refl@{U} x1)) (pr1 pat) x0 (pr2 pat)))) X Y x) y))
     → Id@{U'} c x) : Type@{U'} *)
End Short.

Set Printing Implicit.
Eval compute in isUnivalent@{U U'}.
(*      = forall (X Y : Type@{U})
         (y : {f : X -> Y &
              forall y : Y,
              {c : {x : X & @Id@{U} Y (f x) y} &
              forall x : {x : X & @Id@{U} Y (f x) y},
              @Id@{U} {x0 : X & @Id@{U} Y (f x0) y} c x}}),
       {c
       : {x : @Id@{U'} Type@{U} X Y &
         @Id@{U}
           {f : X -> Y &
           forall y0 : Y,
           {c : {x0 : X & @Id@{U} Y (f x0) y0} &
           forall x0 : {x0 : X & @Id@{U} Y (f x0) y0},
           @Id@{U} {x1 : X & @Id@{U} Y (f x1) y0} c x0}}
           (@J@{U U'} Type@{U}
              (fun (X0 Y0 : Type@{U}) (_ : @Id@{U'} Type@{U} X0 Y0) =>
               {f : X0 -> Y0 &
               forall y0 : Y0,
               {c : {x0 : X0 & @Id@{U} Y0 (f x0) y0} &
               forall x0 : {x0 : X0 & @Id@{U} Y0 (f x0) y0},
               @Id@{U} {x1 : X0 & @Id@{U} Y0 (f x1) y0} c x0}})
              (fun X0 : Type@{U} =>
               (fun x0 : X0 => x0;
               fun x0 : X0 =>
               ((x0; @refl@{U} X0 x0);
               fun pat : {y0 : X0 & @Id@{U} X0 y0 x0} =>
               @J@{U U} X0
                 (fun (y0 x1 : X0) (p : @Id@{U} X0 y0 x1) =>
                  @Id@{U} {y1 : X0 & @Id@{U} X0 y1 x1} 
                    (x1; @refl@{U} X0 x1) (y0; p))
                 (fun x1 : X0 =>
                  @refl@{U} {y0 : X0 & @Id@{U} X0 y0 x1} (x1; @refl@{U} X0 x1))
                 (@pr1 _ _ pat) x0 (@pr2 _ _ pat)))) X Y x) y} &
       forall
         x : {x : @Id@{U'} Type@{U} X Y &
             @Id@{U}
               {f : X -> Y &
               forall y0 : Y,
               {c0 : {x0 : X & @Id@{U} Y (f x0) y0} &
               forall x0 : {x0 : X & @Id@{U} Y (f x0) y0},
               @Id@{U} {x1 : X & @Id@{U} Y (f x1) y0} c0 x0}}
               (@J@{U U'} Type@{U}
                  (fun (X0 Y0 : Type@{U}) (_ : @Id@{U'} Type@{U} X0 Y0) =>
                   {f : X0 -> Y0 &
                   forall y0 : Y0,
                   {c0 : {x0 : X0 & @Id@{U} Y0 (f x0) y0} &
                   forall x0 : {x0 : X0 & @Id@{U} Y0 (f x0) y0},
                   @Id@{U} {x1 : X0 & @Id@{U} Y0 (f x1) y0} c0 x0}})
                  (fun X0 : Type@{U} =>
                   (fun x0 : X0 => x0;
                   fun x0 : X0 =>
                   ((x0; @refl@{U} X0 x0);
                   fun pat : {y0 : X0 & @Id@{U} X0 y0 x0} =>
                   @J@{U U} X0
                     (fun (y0 x1 : X0) (p : @Id@{U} X0 y0 x1) =>
                      @Id@{U} {y1 : X0 & @Id@{U} X0 y1 x1}
                        (x1; @refl@{U} X0 x1) (y0; p))
                     (fun x1 : X0 =>
                      @refl@{U} {y0 : X0 & @Id@{U} X0 y0 x1}
                        (x1; @refl@{U} X0 x1)) (@pr1 _ _ pat) x0
                     (@pr2 _ _ pat)))) X Y x) y},
       @Id@{U'}
         {x0 : @Id@{U'} Type@{U} X Y &
         @Id@{U}
           {f : X -> Y &
           forall y0 : Y,
           {c0 : {x1 : X & @Id@{U} Y (f x1) y0} &
           forall x1 : {x1 : X & @Id@{U} Y (f x1) y0},
           @Id@{U} {x2 : X & @Id@{U} Y (f x2) y0} c0 x1}}
           (@J@{U U'} Type@{U}
              (fun (X0 Y0 : Type@{U}) (_ : @Id@{U'} Type@{U} X0 Y0) =>
               {f : X0 -> Y0 &
               forall y0 : Y0,
               {c0 : {x1 : X0 & @Id@{U} Y0 (f x1) y0} &
               forall x1 : {x1 : X0 & @Id@{U} Y0 (f x1) y0},
               @Id@{U} {x2 : X0 & @Id@{U} Y0 (f x2) y0} c0 x1}})
              (fun X0 : Type@{U} =>
               (fun x1 : X0 => x1;
               fun x1 : X0 =>
               ((x1; @refl@{U} X0 x1);
               fun pat : {y0 : X0 & @Id@{U} X0 y0 x1} =>
               @J@{U U} X0
                 (fun (y0 x2 : X0) (p : @Id@{U} X0 y0 x2) =>
                  @Id@{U} {y1 : X0 & @Id@{U} X0 y1 x2} 
                    (x2; @refl@{U} X0 x2) (y0; p))
                 (fun x2 : X0 =>
                  @refl@{U} {y0 : X0 & @Id@{U} X0 y0 x2} (x2; @refl@{U} X0 x2))
                 (@pr1 _ _ pat) x1 (@pr2 _ _ pat)))) X Y x0) y} c x}
     : Type@{U'} *)