Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* -*- mode: coq; mode: visual-line -*- *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Extensions Factorization.Require Import Truncations.Core Modalities.Modality.LocalOpen Scope path_scope.LocalOpen 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, Escardo, 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]. *)DefinitionFixedBy {X : Type} (f : X -> X) := {x : X & f x = x}.
X: Type f: X -> X H: WeaklyConstant f
IsHProp (FixedBy f)
X: Type f: X -> X H: WeaklyConstant f
IsHProp (FixedBy f)
X: Type f: X -> X H: WeaklyConstant f x0: X p0: f x0 = x0
Contr (FixedBy f)
X: Type f: X -> X H: WeaklyConstant f x0: X p0: f x0 = x0
{x : X & f x0 = x} <~> {x : X & f x = x}
X: Type f: X -> X H: WeaklyConstant f x0: X p0: f x0 = x0
foralla : X, f x0 = a <~> f a = a
X: Type f: X -> X H: WeaklyConstant f x0: X p0: f x0 = x0 x: X
f x0 = x <~> f x = x
X: Type f: X -> X H: WeaklyConstant f x0: X p0: f x0 = x0 x: X
f x = f x0
apply wconst.Defined.(** It follows that if a type [X] admits a weakly constant endofunction [f], then [FixedBy f] is equivalent to [merely X]. *)
X: Type f: X -> X H: WeaklyConstant f
FixedBy f <~> merely X
X: Type f: X -> X H: WeaklyConstant f
FixedBy f <~> merely X
X: Type f: X -> X H: WeaklyConstant f
FixedBy f -> merely X
X: Type f: X -> X H: WeaklyConstant f
merely X -> FixedBy f
X: Type f: X -> X H: WeaklyConstant f
FixedBy f -> merely X
intros [x p]; exact (tr x).
X: Type f: X -> X H: WeaklyConstant f
merely X -> FixedBy f
X: Type f: X -> X H: WeaklyConstant f x: X
FixedBy f
X: Type f: X -> X H: WeaklyConstant f x: X
f (f x) = f x
apply wconst.Defined.(** Therefore, a type is collapsible (admits a weakly constant endomap) if and only if [merely X -> X] (it has "split support"). *)
X: Type H: Collapsible X
merely X -> X
X: Type H: Collapsible X
merely X -> X
X: Type H: Collapsible X
FixedBy collapse -> X
apply pr1.Defined.
X: Type s: merely X -> X
Collapsible X
X: Type s: merely X -> X
Collapsible X
X: Type s: merely X -> X x, y: X
s (tr x) = s (tr y)
apply (ap s), path_ishprop.Defined.(** We say that [f] is *conditionally constant* if it factors through the propositional truncation [merely X], and *constant* if it factors through [Unit]. *)DefinitionConditionallyConstant {XY : 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. *)
X, Y: Type y: Y
ConditionallyConstant (const y)
X, Y: Type y: Y
ConditionallyConstant (const y)
exists (consty); intros x; reflexivity.Defined.(** The type of conditionally constant functions is equivalent to [merely X -> Y]. *)
H: Funext X, Y: Type
{f : X -> Y & ConditionallyConstant f} <~>
(merely X -> Y)
H: Funext X, Y: Type
{f : X -> Y & ConditionallyConstant f} <~>
(merely X -> Y)
H: Funext X, Y: Type
{b : Trunc (-1) X -> Y &
{a : X -> Y & forallx : X, b (tr x) = a x}} <~>
(merely X -> Y)
refine (equiv_sigma_contr _).Defined.(** If a function factors through any hprop, it is conditionally constant. *)
X, Y: Type f: X -> Y P: Type IsHProp0: IsHProp P g: X -> P h: P -> Y p: h o g == f
ConditionallyConstant f
X, Y: Type f: X -> Y P: Type IsHProp0: IsHProp P g: X -> P h: P -> Y p: h o g == f
ConditionallyConstant f
X, Y: Type f: X -> Y P: Type IsHProp0: IsHProp P g: X -> P h: P -> Y p: h o g == f g':= Trunc_rec g : merely X -> P: merely X -> P
ConditionallyConstant f
X, Y: Type f: X -> Y P: Type IsHProp0: IsHProp P g: X -> P h: P -> Y p: h o g == f g':= Trunc_rec g : merely X -> P: merely X -> P x: X
h (g' (tr x)) = f x
apply p.Defined.(** Thus, if it factors through a type that [X] implies is contractible, then it is also conditionally constant. *)
H: 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
H: 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
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f
merely X -> IsHProp P
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f X0: merely X -> IsHProp P
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f
merely X -> IsHProp P
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f
X -> IsHProp P
intros x; pose (Pc x); apply istrunc_succ.
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f X0: merely X -> IsHProp P
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f X0: merely X -> IsHProp P g':= Trunc_ind (fun_ : Trunc (-1) X => P) g
:
merely X -> P: merely X -> P
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y P: Type Pc: X -> Contr P g: X -> P h: P -> Y p: h o g == f X0: merely X -> IsHProp P g':= Trunc_ind (fun_ : Trunc (-1) X => P) g
:
merely X -> P: merely X -> P x: X
h (g' (tr x)) = f x
apply p.Defined.(** Any weakly constant function with collapsible domain is conditionally constant. *)
X, Y: Type f: X -> Y H: Collapsible X H0: WeaklyConstant f
ConditionallyConstant f
X, Y: Type f: X -> Y H: Collapsible X H0: WeaklyConstant f
ConditionallyConstant f
X, Y: Type f: X -> Y H: Collapsible X H0: WeaklyConstant f x: X
f (splitsupp_collapsible (tr x)) = f x
X, Y: Type f: X -> Y H: Collapsible X H0: WeaklyConstant f x: X
f (collapse x) = f x
apply wconst.Defined.(** Any weakly constant function with hset codomain is conditionally constant. *)
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f
merely X -> IsHSet Y
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f
merely X -> IsHSet Y
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f
X -> IsHSet Y
intros x; exact (Ys x).
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
ConditionallyConstant f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
IsHProp (image (Tr (-1)) f)
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
X -> image (Tr (-1)) f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
image (Tr (-1)) f -> Y
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
?h o ?g == f
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
IsHProp (image (Tr (-1)) f)
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y y1: Y p1: Tr (-1) (hfiber f y1) y2: Y p2: Tr (-1) (hfiber f y2)
(y1; p1) = (y2; p2)
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y y1: Y p1: Tr (-1) (hfiber f y1) y2: Y p2: Tr (-1) (hfiber f y2)
y1 = y2
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y y1: Y p1: Tr (-1) (hfiber f y1) y2: Y p2: Tr (-1) (hfiber f y2) X0: IsHSet Y
y1 = y2
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y y1, y2: Y X0: IsHSet Y p2: hfiber f y2 p1: hfiber f y1
y1 = y2
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y y1, y2: Y X0: IsHSet Y x2: X q2: f x2 = y2 x1: X q1: f x1 = y1
y1 = y2
exact (q1^ @ wconst x1 x2 @ q2).
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
X -> image (Tr (-1)) f
apply factor1.
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
image (Tr (-1)) f -> Y
apply factor2.
H: Funext X, Y: Type f: X -> Y Ys: X -> IsHSet Y H0: WeaklyConstant f Ys': merely X -> IsHSet Y
factor2 (image (Tr (-1)) f)
o factor1 (image (Tr (-1)) f) == f
apply fact_factors.Defined.(** We can decompose this into an "induction principle" and its computation rule. *)Definitionmerely_rec_hset `{Funext} {X Y : Type} (f : X -> Y)
`{Ys : X -> IsHSet Y} `{WeaklyConstant _ _ f}
: merely X -> Y
:= (cconst_wconst_hset f).1.Definitionmerely_rec_hset_beta `{Funext} {X Y : Type} (f : X -> Y)
`{Ys : X -> IsHSet Y} `{WeaklyConstant _ _ f}
(x : X)
: merely_rec_hset f (tr x) = f x
:= (cconst_wconst_hset f).2 x.(** More generally, the type of weakly constant functions [X -> Y], when [Y] is a set, is equivalent to [merely X -> Y]. *)
H: Funext X, Y: Type Ys: X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
H: Funext X, Y: Type Ys: X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
H: Funext X, Y: Type Ys: X -> IsHSet Y
merely X -> IsHSet Y
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
H: Funext X, Y: Type Ys: X -> IsHSet Y
merely X -> IsHSet Y
H: Funext X, Y: Type Ys: X -> IsHSet Y
X -> IsHSet Y
intros x; exact (Ys x).
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y g: merely X -> Y
WeaklyConstant (g o tr)
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
(funfc : {x : _ & WeaklyConstant x} =>
merely_rec_hset fc.1)
o (fung : merely X -> Y => (g o tr; ?proj2)) == idmap
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
(fung : merely X -> Y => (g o tr; ?proj2))
o (funfc : {x : _ & WeaklyConstant x} =>
merely_rec_hset fc.1) == idmap
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y g: merely X -> Y
WeaklyConstant (g o tr)
intros x y; apply (ap g), path_ishprop.
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
(funfc : {x : _ & WeaklyConstant x} =>
merely_rec_hset fc.1)
o (fung : merely X -> Y =>
(g o tr;
(funxy : X => ap g (path_ishprop (tr x) (tr y)))
:
WeaklyConstant (g o tr))) == idmap
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y g: merely X -> Y mx: merely X
merely_rec_hset
(funx : X => g (tr x);
funxy : X => ap g (path_ishprop (tr x) (tr y))).1
mx = g mx
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y g: merely X -> Y mx: merely X X0: IsHSet Y
merely_rec_hset
(funx : X => g (tr x);
funxy : X => ap g (path_ishprop (tr x) (tr y))).1
mx = g mx
strip_truncations; reflexivity.
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y
(fung : merely X -> Y =>
(g o tr;
(funxy : X => ap g (path_ishprop (tr x) (tr y)))
:
WeaklyConstant (g o tr)))
o (funfc : {x : _ & WeaklyConstant x} =>
merely_rec_hset fc.1) == idmap
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f
(funx : X => merely_rec_hset (f; proj2).1 (tr x);
funxy : X =>
ap (merely_rec_hset (f; proj2).1)
(path_ishprop (tr x) (tr y))) = (f; proj2)
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f
forallx : X -> Y, IsHProp (WeaklyConstant x)
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f
(funx : X => merely_rec_hset (f; proj2).1 (tr x);
funxy : X =>
ap (merely_rec_hset (f; proj2).1)
(path_ishprop (tr x) (tr y))).1 =
(f; proj2).1
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f
forallx : X -> Y, IsHProp (WeaklyConstant x)
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f f': X -> Y w1, w2: WeaklyConstant f'
w1 = w2
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f f': X -> Y w1, w2: WeaklyConstant f' x, y: X
w1 x y = w2 x y
pose (Ys x); apply path_ishprop.
H: Funext X, Y: Type Ys: X -> IsHSet Y Ys': merely X -> IsHSet Y f: X -> Y proj2: WeaklyConstant f
(funx : X => merely_rec_hset (f; proj2).1 (tr x);
funxy : X =>
ap (merely_rec_hset (f; proj2).1)
(path_ishprop (tr x) (tr y))).1 =
(f; proj2).1