Timings for Constant.v
Require Import HoTT.Basics HoTT.Types.
Require Import Extensions Factorization.
Require Import Truncations.Core Modalities.Modality.
Local Open Scope path_scope.
Local Open Scope trunc_scope.
(** * Varieties of constant function *)
(** Recall that a function [f : X -> Y] is *weakly constant*, [WeaklyConstant f], if [forall x y, f x = f y]. We show, following Kraus, Escardó, Coquand, and Altenkirch, that the type of fixed points of a weakly constant endofunction is an hprop. However, to avoid potential confusion with [Coq.Init.Wf.Fix], instead of their notation [Fix], we denote this type by [FixedBy]. *)
Definition FixedBy {X : Type} (f : X -> X) := {x : X & f x = x}.
Instance ishprop_fix_wconst {X : Type} (f : X -> X)
{wc : WeaklyConstant f}
: IsHProp (FixedBy f).
apply hprop_inhabited_contr; intros [x0 p0].
refine (contr_equiv' {x:X & f x0 = x} _); unfold FixedBy.
apply equiv_functor_sigma_id.
(** It follows that if a type [X] admits a weakly constant endofunction [f], then [FixedBy f] is equivalent to [merely X]. *)
Definition equiv_fix_merely {X : Type} (f : X -> X)
{wc : WeaklyConstant f}
: FixedBy f <~> merely X.
intros [x p]; exact (tr x).
apply Trunc_rec; intros x.
(** Therefore, a type is collapsible (admits a weakly constant endomap) if and only if [merely X -> X] (it has "split support"). *)
Definition splitsupp_collapsible {X} `{Collapsible X}
: merely X -> X.
refine (_ o (equiv_fix_merely collapse)^-1).
Definition collapsible_splitsupp {X} (s : merely X -> X)
: Collapsible X.
refine (Build_Collapsible _ (s o tr) _); intros x y.
apply (ap s), path_ishprop.
(** We say that [f] is *conditionally constant* if it factors through the propositional truncation [merely X], and *constant* if it factors through [Unit]. *)
Definition ConditionallyConstant {X Y : Type} (f : X -> Y)
:= ExtensionAlong (@tr (-1) X) (fun _ => Y) f.
(** We don't yet have a need for a predicate [Constant] on functions; we do already have the operation [const] which constructs the constant function at a given point. Every such constant function is, of course, conditionally constant. *)
Definition cconst_const {X Y} (y : Y)
: ConditionallyConstant (@const X Y y).
exists (const y); intros x; reflexivity.
(** The type of conditionally constant functions is equivalent to [merely X -> Y]. *)
Definition equiv_cconst_from_merely `{Funext} (X Y : Type)
: { f : X -> Y & ConditionallyConstant f } <~> (merely X -> Y).
refine (_ oE (equiv_sigma_symm _)).
exact (equiv_sigma_contr _).
(** If a function factors through any hprop, it is conditionally constant. *)
Definition cconst_factors_hprop {X Y : Type} (f : X -> Y)
(P : Type) `{IsHProp P}
(g : X -> P) (h : P -> Y) (p : h o g == f)
: ConditionallyConstant f.
pose (g' := Trunc_rec g : merely X -> P).
exists (h o g'); intros x.
(** Thus, if it factors through a type that [X] implies is contractible, then it is also conditionally constant. *)
Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y)
(P : Type) {Pc : X -> Contr P}
(g : X -> P) (h : P -> Y) (p : h o g == f)
: ConditionallyConstant f.
assert (merely X -> IsHProp P).
intros x; pose (Pc x); exact istrunc_succ.
pose (g' := Trunc_ind (fun _ => P) g : merely X -> P).
exists (h o g'); intros x.
(** Any weakly constant function with collapsible domain is conditionally constant. *)
Definition cconst_wconst_collapsible {X Y : Type} `{Collapsible X}
(f : X -> Y) {wc : WeaklyConstant f}
: ConditionallyConstant f.
exists (f o splitsupp_collapsible); intros x.
unfold splitsupp_collapsible; simpl.
(** The image of a weakly constant function with hset codomain is an hprop. In fact, we just need to assume that [merely X -> IsHSet Y]. *)
Local Instance hprop_image_wconst_hset_if_merely_domain {X Y : Type} (f : X -> Y)
{Ys : merely X -> IsHSet Y} {wc: WeaklyConstant f}
: IsHProp (image (-1) f).
apply path_sigma_hprop; cbn.
destruct m as [x p], m' as [x' p'].
exact (p^ @ wc x x' @ p').
(** When [merely X -> IsHSet Y], any weakly constant function [X -> Y] is conditionally constant. *)
Definition cconst_wconst_hset_if_merely_domain {X Y : Type} (f : X -> Y)
{Ys : merely X -> IsHSet Y} {wc: WeaklyConstant f}
: ConditionallyConstant f.
srapply (cconst_factors_hprop f (image (-1) f)).
(** The previous result will be most often used when we know [Y] is an hset, so we specialize to this case. *)
Definition cconst_wconst_hset {X Y : Type} (f : X -> Y)
{Ys : IsHSet Y} {wc : WeaklyConstant f}
: ConditionallyConstant f
:= cconst_wconst_hset_if_merely_domain f (Ys:=fun _ => Ys).
(** We can decompose this into an "induction principle" and its computation rule. *)
Definition merely_rec_hset {X Y : Type} (f : X -> Y)
{Ys : IsHSet Y} {wc : WeaklyConstant f}
: merely X -> Y
:= (cconst_wconst_hset f).1.
(** The computation rule is [(cconst_wconst_hset f).2 x], but that's reflexivity. *)
Definition merely_rec_hset_beta {X Y : Type} (f : X -> Y)
{Ys : IsHSet Y} {wc : WeaklyConstant f}
(x : X)
: merely_rec_hset f (tr x) = f x
:= idpath.
(** If we assume [Funext], then we can weaken the hypothesis from [merely X -> IsHSet Y] to [X -> IsHSet Y], since with [Funext], we know that [IsHSet Y] is an hprop. *)
Definition cconst_wconst_hset_if_domain `{Funext} {X Y : Type} (f : X -> Y)
{Ys : X -> IsHSet Y} {wc : WeaklyConstant f}
: ConditionallyConstant f
:= cconst_wconst_hset_if_merely_domain f (Ys:=Trunc_rec Ys).
(** We record the corresponding induction principle, but not the computation principle, since it is again definitional. *)
Definition merely_rec_hset_if_domain `{Funext} {X Y : Type} (f : X -> Y)
{Ys : X -> IsHSet Y} {wc : WeaklyConstant f}
: merely X -> Y
:= (cconst_wconst_hset_if_domain f).1.
(** The type of weakly constant functions [X -> Y], when [Y] is a set, is equivalent to [merely X -> Y]. This uses [Funext] for the main argument, so we may as well state it with the more general assumption [X -> IsHSet Y]. *)
Definition equiv_merely_rec_hset_if_domain `{Funext} (X Y : Type)
{Ys : X -> IsHSet Y}
: { f : X -> Y & WeaklyConstant f } <~> (merely X -> Y).
pose proof (Ys' := Trunc_rec Ys : merely X -> IsHSet Y).
snapply equiv_adjointify.
exact (merely_rec_hset_if_domain f (wc:=wc)).
intros x y; apply (ap g), path_ishprop.
intros g; apply path_arrow; intros mx.
strip_truncations; reflexivity.
pose (Ys x); apply path_ishprop.
(** We can use the above to give a funext-free approach to defining a map by factoring through a surjection. *)
Section SurjectiveFactor.
Context {A B C : Type} `{IsHSet C} (f : A -> C) (g : A -> B)
(resp : forall x y, g x = g y -> f x = f y).
(** The assumption [resp] tells us that [f o pr1] is weakly constant on each fiber of [g], so it factors through the propositional truncation. *)
Definition surjective_factor_aux (b : B) : merely (hfiber g b) -> C.
rapply (merely_rec_hset (f o pr1)).
exact (resp x y (p @ q^)).
(** When [g] is surjective, those propositional truncations are contractible, giving us a way to get an element of [C]. *)
Definition surjective_factor `{IsSurjection g} : B -> C.
exact (surjective_factor_aux b (center _)).
Definition surjective_factor_factors `{IsSurjection g}
: surjective_factor o g == f.
intros a; unfold surjective_factor.
exact (ap (surjective_factor_aux (g a)) (contr (tr (a; idpath)))).