Library HoTT.Homotopy.EvaluationFibration

From HoTT Require Import Basics Types Truncations.Core Pointed.Core Homotopy.Cover.

Local Open Scope pointed_scope.
Local Open Scope trunc_scope.

Evaluation fibrations and self-maps

(* The type of unpointed self maps of A, pointed at the identity map. *)
Definition selfmaps (A : Type) : pType := [A → A , idmap ].

The unrestricted evaluation map.

Definition ev (A : pType) : selfmaps A ->* A
:= Build_pMap _ _ (fun f : selfmaps A ⇒ f pt) idpath.

The evaluation fibration of an unpointed map X → A.

Definition evfib {X : pType} {A : Type} (f : X → A) : comp (X → A) (tr f) → A
:= fun g ⇒ g .1 pt.

If f is pointed, then the evaluation fibration of f is too.

Definition pevfib {A X : pType} (f : X ->* A) : pcomp (X → A) f ->* A
:= Build_pMap _ _ (fun g : pcomp (X → A) f ⇒ g .1 pt) (point_eq f).

(* The evaluation map of the identity. *)
Definition ev1 (A : pType) := pevfib (A:=A) pmap_idmap.