Require Import HoTT.Basics Types.Universe.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
IsEquiv (fmap F f)
Proof.
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
IsEquiv (fmap F f)
  refine (equiv_induction (fun A' e => IsEquiv (fmap F e)) _ _ (Build_Equiv _ _ f _)).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
IsEquiv (fmap F 1%equiv)
  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)).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
fmap F f =
equiv_path (F A) (F B) (ap F (path_universe f))
Proof.
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
fmap F f =
equiv_path (F A) (F B) (ap F (path_universe f))
  refine (equiv_induction
    (fun A' e => fmap F e = equiv_path _ _ (ap F (path_universe e)))
    _ _ (Build_Equiv _ _ f _)).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
fmap F 1%equiv =
equiv_path (F A) (F A) (ap F (path_universe 1%equiv))
  transitivity (idmap : F A -> F A).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
fmap F 1%equiv = (idmap : F A -> F A)
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
(idmap : F A -> F A) =
equiv_path (F A) (F A) (ap F (path_universe 1%equiv))
  -
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
fmap F 1%equiv = (idmap : F A -> F A) apply fmap_idmap.
  -
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
(idmap : F A -> F A) =
equiv_path (F A) (F A) (ap F (path_universe 1%equiv)) change (equiv_idmap A) with (equiv_path A A 1).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
(idmap : F A -> F A) =
equiv_path (F A) (F A)
  (ap F (path_universe (equiv_path A A 1)))
    rewrite (@eta_path_universe _ A A 1).
H: Univalence
F: Type -> Type
FF: Functorish F
A, B: Type
f: A -> B
H0: IsEquiv f
idmap = equiv_path (F A) (F A) (ap F 1) exact 1.
Defined.

End Functorish.