"Compilation" of univalence in Coq.

gistfile1.coq

Require Import MirrorCore.Iso.

Set Implicit Arguments.
Set Strict Implicit.

Definition Pi (T : Type) (F : T -> Type) : Type :=
  forall x : T, F x.

(** What is the generalization of [Functor] to a dependent function? **)
Class DFunctor (Q : Type -> Type) (F : Pi Q)
      (Hiso : IsoFunctor Q)
      (equiv : forall x, Q x -> Q x -> Type) (** TODO: this is odd... **)
: Type :=
{ fdmap : forall A B : Type,
          forall i : Iso A B, equiv _ (F A) (@outof _ _ (@fmap Iso Q Hiso _ _ i) (F B))
}.

Definition IsoIso A : IsoFunctor (fun x : Type => Iso A x -> Type).
constructor; intros.
constructor. intros.
apply X0. eapply Iso_compose. apply Iso_flip. eassumption. assumption.
intros. apply X0. eapply Iso_compose. eapply X. eassumption.
Defined.

Lemma iso_compose_id : forall A B (i : Iso A B), i = Iso_compose i (Iso_ident _).
unfold Iso_compose. simpl. unfold compose.
(** eta for records would give you this equation without a match! **)
destruct i. reflexivity.
Defined.

Definition Iso_rect
           (A : Type)
           (P : forall B, Iso A B -> Type)
           (IsoDFunctor : @DFunctor (fun x => Iso A x -> Type) P (IsoIso _) (fun x a b => forall i, Iso (a i) (b i)))
           (br : P A (Iso_ident A))
           (B : Type) (pf : Iso A B) : P B pf.
rewrite (iso_compose_id pf).
revert br.
exact (@into _ _ (@fdmap _ _ _ _ IsoDFunctor A B pf (Iso_ident _))).
Show Proof.
Defined.

(** NOTE: If Iso wasn't a record then this would simplify completely *)
Eval cbv beta iota zeta delta [Iso_rect eq_rect_r eq_rect eq_sym Iso_ident IsoIso into outof fdmap iso_compose_id ] in Iso_rect.