Timings for ConstantDiagram.v
(** * Constant diagram *)
Definition diagram_const (C : Type) : Diagram G.
Definition diagram_const_functor {A B : Type} (f : A -> B)
: DiagramMap (diagram_const A) (diagram_const B).
srapply Build_DiagramMap.
Definition diagram_const_functor_comp {A B C : Type}
(f : A -> B) (g : B -> C)
: diagram_const_functor (g o f)
= diagram_comp (diagram_const_functor g) (diagram_const_functor f).
Definition diagram_const_functor_idmap {A : Type}
: diagram_const_functor (idmap : A -> A) = diagram_idmap (diagram_const A).
Definition equiv_diagram_const_cocone `{Funext} (D : Diagram G) (X : Type)
: DiagramMap D (diagram_const X) <~> Cocone D X.
srapply equiv_adjointify.
1,2: intros [? w]; econstructor.
1,2: intros x y z z'; symmetry; revert x y z z'.
3: srapply path_DiagramMap.
all: cbn; intros; hott_simpl.
Definition equiv_diagram_const_cone `{Funext} (X : Type) (D : Diagram G)
: DiagramMap (diagram_const X) D <~> Cone X D.
srapply equiv_adjointify.
1,2: intros [? w]; econstructor.
3: srapply path_DiagramMap.
all: cbn; intros; hott_simpl.