Merge pull request #2126 from jdchristensen/constant-improvements

Constant.v: variants without Funext; cleanups
HoTT · Oct 26, 2024 · d25ab6e · d25ab6e
2 parents 67958a1 + f2151bc
commit d25ab6e
Show file tree

Hide file tree

Showing 2 changed files with 79 additions and 55 deletions.
diff --git a/theories/Constant.v b/theories/Constant.v
@@ -12,8 +12,8 @@ Local Open Scope trunc_scope.
 Definition FixedBy {X : Type} (f : X -> X) := {x : X & f x = x}.
 
 Global Instance ishprop_fix_wconst {X : Type} (f : X -> X)
-       `{WeaklyConstant _ _ f}
-: IsHProp (FixedBy f).
+  {wc : WeaklyConstant f}
+  : IsHProp (FixedBy f).
 Proof.
   apply hprop_inhabited_contr; intros [x0 p0].
   refine (contr_equiv' {x:X & f x0 = x} _); unfold FixedBy.
@@ -24,8 +24,8 @@ Defined.
 
 (** 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)
-           `{WeaklyConstant _ _ f}
-: FixedBy f <~> merely X.
+  {wc : WeaklyConstant f}
+  : FixedBy f <~> merely X.
 Proof.
   apply equiv_iff_hprop.
   - intros [x p]; exact (tr x).
@@ -36,14 +36,14 @@ Defined.
 
 (** 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.
+  : merely X -> X.
 Proof.
   refine (_ o (equiv_fix_merely collapse)^-1).
   apply pr1.
 Defined.
 
 Definition collapsible_splitsupp {X} (s : merely X -> X)
-: Collapsible X.
+  : Collapsible X.
 Proof.
   refine (Build_Collapsible _ (s o tr) _); intros x y.
   apply (ap s), path_ishprop.
@@ -56,24 +56,24 @@ Definition ConditionallyConstant {X Y : Type} (f : X -> Y)
 
 (** 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).
+  : ConditionallyConstant (@const X Y y).
 Proof.
   exists (const y); intros x; reflexivity.
 Defined.
 
 (** 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).
+  : { f : X -> Y & ConditionallyConstant f } <~> (merely X -> Y).
 Proof.
   refine (_ oE (equiv_sigma_symm _)).
   refine (equiv_sigma_contr _).
 Defined.
 
 (** 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.
+  (P : Type) `{IsHProp P}
+  (g : X -> P) (h : P -> Y) (p : h o g == f)
+  : ConditionallyConstant f.
 Proof.
   pose (g' := Trunc_rec g : merely X -> P).
   exists (h o g'); intros x.
@@ -82,9 +82,9 @@ Defined.
 
 (** 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.
+  (P : Type) {Pc : X -> Contr P}
+  (g : X -> P) (h : P -> Y) (p : h o g == f)
+  : ConditionallyConstant f.
 Proof.
   assert (merely X -> IsHProp P).
   { apply Trunc_rec.            (** Uses funext *)
@@ -95,64 +95,88 @@ Proof.
 Defined.
 
 (** Any weakly constant function with collapsible domain is conditionally constant. *)
-Definition cconst_wconst_collapsible {X Y : Type} (f : X -> Y)
-           `{Collapsible X} `{WeaklyConstant _ _ f}
-: ConditionallyConstant f.
+Definition cconst_wconst_collapsible {X Y : Type} `{Collapsible X}
+  (f : X -> Y) {wc : WeaklyConstant f}
+  : ConditionallyConstant f.
 Proof.
   exists (f o splitsupp_collapsible); intros x.
   unfold splitsupp_collapsible; simpl.
   apply wconst.
 Defined.
 
-(** Any weakly constant function with hset codomain is conditionally constant. *)
-Definition cconst_wconst_hset `{Funext} {X Y : Type} (f : X -> Y)
-           `{Ys : X -> IsHSet Y} `{WeaklyConstant _ _ f}
-: ConditionallyConstant f.
+(** 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).
 Proof.
-  assert (Ys' : merely X -> IsHSet Y).
-  { apply Trunc_rec. intros x; exact (Ys x). }
-  simple refine (cconst_factors_hprop f (image (-1) f) _ _ _).
-  - apply hprop_allpath; intros [y1 p1] [y2 p2].
-    apply path_sigma_hprop; simpl.
-    pose proof (Ys' (Trunc_functor (-1) pr1 p1)).
-    strip_truncations.
-    destruct p1 as [x1 q1], p2 as [x2 q2].
-    exact (q1^ @ wconst x1 x2 @ q2).
+  apply hprop_allpath.
+  intros [b m] [b' m'].
+  apply path_sigma_hprop; cbn.
+  assert (Ys' : IsHSet Y).
+  { apply Ys. strip_truncations. exact (tr m.1). }
+  strip_truncations.
+  destruct m as [x p], m' as [x' p'].
+  exact (p^ @ wc x x' @ p').
+Defined.
+
+(** 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.
+Proof.
+  srapply (cconst_factors_hprop f (image (-1) f)).
   - apply factor1.
   - apply factor2.
   - apply fact_factors.
 Defined.
 
+(** 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 `{Funext} {X Y : Type} (f : X -> Y)
-           `{Ys : X -> IsHSet Y} `{WeaklyConstant _ _ f}
-: merely X -> Y
+Definition merely_rec_hset {X Y : Type} (f : X -> Y)
+  {Ys : IsHSet Y} {wc : WeaklyConstant f}
+  : merely X -> Y
   := (cconst_wconst_hset f).1.
 
-Definition merely_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]. *)
-Definition equiv_merely_rec_hset `{Funext} (X Y : Type)
-           `{Ys : X -> IsHSet Y}
-: { f : X -> Y & WeaklyConstant f } <~> (merely X -> Y).
+(** 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).
 Proof.
-  assert (Ys' : merely X -> IsHSet Y).
-  { apply Trunc_rec. intros x; exact (Ys x). }
-  simple refine (equiv_adjointify
-            (fun fc => @merely_rec_hset _ _ _ fc.1 _ fc.2)
-            (fun g => (g o tr ; _)) _ _); try exact _.
-  - intros x y; apply (ap g), path_ishprop.
+  pose proof (Ys' := Trunc_rec Ys : merely X -> IsHSet Y).
+  snrapply equiv_adjointify.
+  - intros [f wc].  exact (merely_rec_hset_if_domain f (wc:=wc)).
+  - intro g.  exists (g o tr).
+    intros x y; apply (ap g), path_ishprop.
   - intros g; apply path_arrow; intros mx.
     pose proof (Ys' mx).
     strip_truncations; reflexivity.
-  - intros [f ?].
-    refine (path_sigma_hprop _ _ _).
-    + intros f'; apply hprop_allpath; intros w1 w2.
-      apply path_forall; intros x; apply path_forall; intros y.
+  - intros [f wc].
+    snrapply path_sigma; cbn.
+    + reflexivity.
+    + cbn. funext x y.
       pose (Ys x); apply path_ishprop.
-    + apply path_arrow; intros x; reflexivity.
 Defined.
diff --git a/theories/Universes/BAut.v b/theories/Universes/BAut.v
@@ -111,7 +111,7 @@ Proof.
   refine ((equiv_functor_forall'
              (P := fun Z => { f : (Z=X) -> P Z & WeaklyConstant f })
              1
-             (fun Z => equiv_merely_rec_hset _ _)) oE _); simpl.
+             (fun Z => equiv_merely_rec_hset_if_domain _ _)) oE _); simpl.
   { intros p. change (IsHSet (P (BAut_pr1 X (Z ; tr p)))). exact _. }
   unfold WeaklyConstant.
   (** Now we peel away a bunch of contractible types. *)