From 883a8684efd7b2b814cfc499ace0d0cb9e13a9e7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 16:29:55 +0100 Subject: [PATCH] another naming conflict `is-pullback-cartesian-product` --- .../universal-property-cartesian-product-types.lagda.md | 6 +++--- src/synthetic-homotopy-theory/acyclic-maps.lagda.md | 2 +- .../truncated-acyclic-maps.lagda.md | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index 398f26853a..362ce03044 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -108,9 +108,9 @@ Cartesian products are a special case of pullbacks. is-retraction-inv-gap-product (pair a b) = refl abstract - is-pullback-product : + is-pullback-cartesian-product : is-pullback (terminal-map A) (terminal-map B) cone-product - is-pullback-product = + is-pullback-cartesian-product = is-equiv-is-invertible inv-gap-product is-section-inv-gap-product @@ -131,5 +131,5 @@ We conclude that cartesian products satisfy the universal property of pullbacks. ( terminal-map A) ( terminal-map B) ( cone-product) - ( is-pullback-product) + ( is-pullback-cartesian-product) ``` diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index f10cf0df03..98f0df2cb7 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -494,7 +494,7 @@ module _ ( terminal-map A) ( terminal-map B) ( cone-product A B) - ( is-pullback-product A B) + ( is-pullback-cartesian-product A B) ( is-acyclic-map-terminal-map-is-acyclic A ac-A))) ``` diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index 74b92b82ab..7c38195588 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -470,7 +470,7 @@ module _ ( terminal-map A) ( terminal-map B) ( cone-product A B) - ( is-pullback-product A B) + ( is-pullback-cartesian-product A B) ( is-truncated-acyclic-map-terminal-map-is-truncated-acyclic A ac-A))) ```