Require Import HoTT.Basics Types.Universe.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).
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)
  exact (transport _ (fmap_idmap F)^ _).
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.