Timings for Functorish.v

Require Import HoTT.Basics Types.Universe.

Local Open Scope path_scope.

Section Functorish.

Context `{Univalence}.

(* We do not need composition to be preserved. *)

Class Functorish (F : Type -> Type) := {
  fmap {A B} (f : A -> B) : F A -> F B ;
  fmap_idmap (A:Type) : fmap (idmap : A -> A) = idmap
}.

Global Arguments fmap F {FF} {A B} f _ : rename.

Global Arguments fmap_idmap F {FF A} : rename.

Context (F : Type -> Type).

Context {FF : Functorish F}.

Proposition isequiv_fmap {A B} (f : A -> B) `{IsEquiv _ _ f}
  : IsEquiv (fmap F f).

Proof.

  refine (equiv_induction (fun A' e => IsEquiv (fmap F e)) _ _ (Build_Equiv _ _ f _)).

  refine (transport _ (fmap_idmap F)^ _);
    try apply isequiv_idmap.

 (* This line may not be needed in a new enough coq. *)

Defined.

Proposition fmap_agrees_with_univalence {A B} (f : A -> B) `{IsEquiv _ _ f}
  : fmap F f = equiv_path _ _ (ap F (path_universe f)).

Proof.

  refine (equiv_induction
    (fun A' e => fmap F e = equiv_path _ _ (ap F (path_universe e)))
    _ _ (Build_Equiv _ _ f _)).

  transitivity (idmap : F A -> F A).

  -

 apply fmap_idmap.

  -

 change (equiv_idmap A) with (equiv_path A A 1).

    rewrite (@eta_path_universe _ A A 1).

 exact 1.

Defined.

End Functorish.