Refactor function actions on cauchy approximations #1738

malarbol · 2025-12-01T18:54:05Z

This PR introduces the new modules:

action-of-isometries-on-cauchy-approximations-pseudometric-spaces.lagda.md;
action-of-short-maps-on-cauchy-approximations-metric-spaces.lagda.md;
action-of-short-maps-on-cauchy-approximations-pseudometric-spaces.lagda.md.

to refactor these concepts in their own modules.

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

--lossy-unification breaks some proof of UniMath#1726

malarbol · 2025-12-01T18:56:40Z

Because we didn't have Cauchy pseudocompletions at the time, the definitions of these actions were in the cauchy-approximations-XXX modules while the fact that they induce short maps / isometries were in the cauchy-pseudocompletions-XXX modules.

fredrik-bakke · 2025-12-03T21:39:08Z

action-of-isometries-on-cauchy-approximations-pseudometric-spaces.lagda.md;

action-of-short-maps-on-cauchy-approximations-metric-spaces.lagda.md;

action-of-short-maps-on-cauchy-approximations-pseudometric-spaces.lagda.md.

The conventional way to name such files in agda-unimath is e.g. action-on-cauchy-approximations-of-isometries-pseudometric-spaces. This also mirrors how the basic definitions themselves are named, e.g., map-cauchy-approximation-isometry-Pseudometric-Space I guess

fredrik-bakke · 2025-12-03T21:39:47Z

src/metric-spaces/action-of-isometries-on-cauchy-approximations-pseudometric-spaces.lagda.md

@@ -0,0 +1,143 @@
+# The action of isometries on Cauchy approximations in pseudometric spaces


Suggested change

# The action of isometries on Cauchy approximations in pseudometric spaces

# The action on Cauchy approximations of isometries between pseudometric spaces

fredrik-bakke · 2025-12-03T21:40:10Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-metric-spaces.lagda.md

@@ -0,0 +1,92 @@
+# The action of short maps on Cauchy approximations in metric spaces


Suggested change

# The action of short maps on Cauchy approximations in metric spaces

# The action on Cauchy approximations of short maps between metric spaces

fredrik-bakke · 2025-12-03T21:40:24Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-pseudometric-spaces.lagda.md

@@ -0,0 +1,97 @@
+# The action of short maps on Cauchy approximations in pseudometric spaces


Suggested change

# The action of short maps on Cauchy approximations in pseudometric spaces

# The action on Cauchy approximations of short maps between pseudometric spaces

fredrik-bakke · 2025-12-03T21:40:57Z

src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md

        ( metric-quotient-Pseudometric-Space M))
  short-map-metric-quotient-cauchy-apprtoximation-Pseudometric-Space =
-    short-map-short-function-cauchy-approximation-Pseudometric-Space
+    short-map-cauchy-approximation-short-function-Pseudometric-Space


this highlights that short-function should be renamed to short-map

fredrik-bakke · 2025-12-03T21:43:41Z

src/metric-spaces/cauchy-pseudocompletion-of-metric-spaces.lagda.md

      ( is-limit-map-lim-cauchy-pseudocompletion-is-complete-Metric-Space u)
 ```
+
+### The isometry from the Cauchy pseudocompletion of a complete metric space to its limit


This sentence doesn't make sense. There is no "map" from a complete metric space to its limit. What you exhibit an isometry between is the two

( cauchy-pseudocompletion-Metric-Space M) ( pseudometric-Metric-Space M)

fredrik-bakke · 2025-12-03T21:47:33Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-pseudometric-spaces.lagda.md

+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on their
+[cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce a short map between their
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).


Suggested change

[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on their

[cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)

and induce a short map between their

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).

[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on

[cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)

and induce a short map between the

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).

fredrik-bakke · 2025-12-03T21:48:11Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-pseudometric-spaces.lagda.md

action-on-cauchy-approximations-short-maps-pseudometric-spaces

fredrik-bakke · 2025-12-03T21:48:43Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-metric-spaces.lagda.md

+[Short maps](metric-spaces.short-functions-metric-spaces.md) between
+[metric spaces](metric-spaces.metric-spaces.md) act on their
+[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md)
+and induce a short map between their
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md).


Suggested change

[Short maps](metric-spaces.short-functions-metric-spaces.md) between

[metric spaces](metric-spaces.metric-spaces.md) act on their

[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md)

and induce a short map between their

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md).

[metric spaces](metric-spaces.metric-spaces.md) act on

[cauchy approximations](metric-spaces.cauchy-approximations-metric-spaces.md)

and induce a short map between the

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-metric-spaces.md).

fredrik-bakke · 2025-12-03T21:49:13Z

src/metric-spaces/action-of-short-maps-on-cauchy-approximations-metric-spaces.lagda.md

action-on-cauchy-approximations-short-maps-metric-spaces.lagda.md

fredrik-bakke · 2025-12-03T21:49:45Z

src/metric-spaces/action-of-isometries-on-cauchy-approximations-pseudometric-spaces.lagda.md

action-on-cauchy-approximations-isometries-pseudometric-spaces.lagda.md

fredrik-bakke · 2025-12-03T21:50:10Z

src/metric-spaces/action-of-isometries-on-cauchy-approximations-pseudometric-spaces.lagda.md

+[Isometries](metric-spaces.isometries-pseudometric-spaces.md) between
+[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on their
+[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)
+and induce an isometry between their
+[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).


Suggested change

[Isometries](metric-spaces.isometries-pseudometric-spaces.md) between

[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on their

[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)

and induce an isometry between their

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).

[Isometries](metric-spaces.isometries-pseudometric-spaces.md) between

[pseudometric spaces](metric-spaces.pseudometric-spaces.md) act on

[Cauchy approximations](metric-spaces.cauchy-approximations-pseudometric-spaces.md)

and induce an isometry between the

[Cauchy pseudocompletions](metric-spaces.cauchy-pseudocompletion-of-pseudometric-spaces.md).

fredrik-bakke · 2025-12-03T21:52:01Z

...ric-spaces/cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md

+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces where


Suggested change

module metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces where

module

metric-spaces.cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces

where

fredrik-bakke · 2025-12-03T21:52:58Z

...ric-spaces/cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md

+    ( map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space ,
+      is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space)
+
+  is-limit-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :


seems like it should be marked abstract

fredrik-bakke · 2025-12-03T21:53:11Z

...ric-spaces/cauchy-approximations-in-cauchy-pseudocompletions-of-pseudometric-spaces.lagda.md

+    in
+      map-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space d₂ d₁
+
+  is-cauchy-map-lim-cauchy-approximation-cauchy-pseudocompletion-Pseudometric-Space :


seems like this should be marked abstract

fredrik-bakke

Since you're already taking the opportunity to fix some names across the board, would you be so kind to also change the naming pattern short-function- to short-map-?

malarbol and others added 25 commits November 22, 2025 18:28

misc results

6508a94

metric extensions

02e4ae0

unused imports

d36ea7a

refactor

03c3e2b

isometries between metric extensions

7a21f12

fix link

4afd6bd

rephrase header

9fe2c5f

Update src/metric-spaces/isometries-between-metric-extensions-of-pseu…

83610c8

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

Update src/metric-spaces/isometries-between-metric-extensions-of-pseu…

57e8c80

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

Update src/metric-spaces/isometries-between-metric-extensions-of-pseu…

f955463

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

Update src/metric-spaces/isometries-between-metric-extensions-of-pseu…

898e0b0

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

fix names

7e0a1f3

fix names isometry-Metric-Extension

621ab65

shorter name

aebfd7e

Update src/metric-spaces/isometries-between-metric-extensions-of-pseu…

78d2866

…dometric-spaces.lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

import whiskering

3b1d036

fix name id-isometry-XX

dc35782

fix name id-short-function-XX

d0bc999

forgetful metric extensions of metric spaces

ba5385e

plural (preserves|reflects)-neighborhoods-XXX

fd43093

remove --lossy-unification

1e8202c

--lossy-unification breaks some proof of UniMath#1726

Merge branch 'master' into metric-extensions

6f601dd

Merge branch 'master' into metric-extensions

81a70be

Merge branch 'master' into metric-extensions

55d66a4

refactor action of functions

4b1c84f

malarbol added the metric-spaces label Dec 1, 2025

malarbol added 2 commits December 1, 2025 19:57

fix link

3f01f29

fix link

a48c9a7

malarbol changed the title ~~Refactor function actions cauchy approximations~~ Refactor function actions on cauchy approximations Dec 2, 2025

remove metric extensions

4979c51

malarbol mentioned this pull request Dec 2, 2025

Metric extensions #1742

Open

fredrik-bakke reviewed Dec 3, 2025

View reviewed changes

fredrik-bakke approved these changes Dec 3, 2025

View reviewed changes

		@@ -0,0 +1,143 @@
		# The action of isometries on Cauchy approximations in pseudometric spaces

	# The action of isometries on Cauchy approximations in pseudometric spaces
	# The action on Cauchy approximations of isometries between pseudometric spaces

		@@ -0,0 +1,92 @@
		# The action of short maps on Cauchy approximations in metric spaces

		@@ -0,0 +1,97 @@
		# The action of short maps on Cauchy approximations in pseudometric spaces

Refactor function actions on cauchy approximations #1738

Are you sure you want to change the base?

Refactor function actions on cauchy approximations #1738

Uh oh!

Conversation

malarbol commented Dec 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

malarbol commented Dec 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fredrik-bakke commented Dec 3, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fredrik-bakke Dec 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fredrik-bakke left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

malarbol commented Dec 1, 2025 •

edited

Loading

malarbol commented Dec 1, 2025 •

edited

Loading

fredrik-bakke Dec 3, 2025 •

edited

Loading