From a503a136856d9c658af1b2ec57bffea3154bb4df Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 18 Nov 2024 22:09:03 -0500 Subject: [PATCH] better name for bpwedge point --- CHANGELOG_UNRELEASED.md | 2 +- theories/homotopy_theory/wedge_sigT.v | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 584b6de91..a30d21b64 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -116,7 +116,7 @@ + new definitions `reparameterize`, `mk_path`, and `chain_path`. + new lemmas `path_eqP`, and `chain_path_cts_point`. - in file `homotopy_theory/wedge_sigT.v`, - + new definition `wedge2p`. + + new definition `bpwedge_shared_pt`. + new notations `bpwedge`, and `bpwedge_lift`. ### Changed diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 8bc9180ab..86822e545 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -24,8 +24,9 @@ From mathcomp Require Import separation_axioms function_spaces. (* wedge_prod == the mapping from the wedge as a quotient of sums to *) (* the wedge as a subspace of the product topology. *) (* It's an embedding when the index is finite. *) +(* bpwedge_shared_pt b == the shared point in the bpwedge. Either zero or one *) +(* depending on `b`. *) (* bpwedge == wedge of two bipointed spaces gluing zero to one *) -(* wedge2p == the shared point in the bpwedge *) (* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) (* *) @@ -390,10 +391,10 @@ End pwedge. Section bpwedge. Context (X Y : bpTopologicalType). -Definition wedge2p b := +Definition bpwedge_shared_pt b := if b return (if b then X else Y) then @one X else @zero Y. -Local Notation bpwedge := (@wedge bool _ wedge2p). -Local Notation bpwedge_lift := (@wedge_lift bool _ wedge2p). +Local Notation bpwedge := (@wedge bool _ bpwedge_shared_pt). +Local Notation bpwedge_lift := (@wedge_lift bool _ bpwedge_shared_pt). Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one. Proof. @@ -407,5 +408,5 @@ HB.instance Definition _ := @isBiPointed.Build bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. End bpwedge. -Notation bpwedge X Y := (@wedge bool _ (wedge2p X Y)). -Notation bpwedge_lift X Y := (@wedge_lift bool _ (wedge2p X Y)). +Notation bpwedge X Y := (@wedge bool _ (bpwedge_shared_pt X Y)). +Notation bpwedge_lift X Y := (@wedge_lift bool _ (bpwedge_shared_pt X Y)).