From e9d7cceae4642c7189b7fc2c6387bae0c4000e6f Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Tue, 16 Jan 2024 13:02:46 +0100 Subject: [PATCH] `reflexive-htpy-...` -> `refl-htpy-...` --- .../cocones-under-sequential-diagrams.lagda.md | 8 ++++---- .../dependent-cocones-under-sequential-diagrams.lagda.md | 8 ++++---- .../morphisms-sequential-diagrams.lagda.md | 8 ++++---- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md index a0cd52d13f..125edcfcaf 100644 --- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md @@ -203,16 +203,16 @@ module _ ( c : cocone-sequential-diagram A X) where - reflexive-htpy-cocone-sequential-diagram : + refl-htpy-cocone-sequential-diagram : htpy-cocone-sequential-diagram c c - pr1 reflexive-htpy-cocone-sequential-diagram n = refl-htpy - pr2 reflexive-htpy-cocone-sequential-diagram n = right-unit-htpy + pr1 refl-htpy-cocone-sequential-diagram n = refl-htpy + pr2 refl-htpy-cocone-sequential-diagram n = right-unit-htpy htpy-eq-cocone-sequential-diagram : ( c' : cocone-sequential-diagram A X) → ( c ＝ c') → htpy-cocone-sequential-diagram c c' htpy-eq-cocone-sequential-diagram .c refl = - reflexive-htpy-cocone-sequential-diagram + refl-htpy-cocone-sequential-diagram abstract is-torsorial-htpy-cocone-sequential-diagram : diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md index 2fb6c8cfd7..5cb933ac9b 100644 --- a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md @@ -191,17 +191,17 @@ module _ { c : cocone-sequential-diagram A X} (P : X → UU l3) where - reflexive-htpy-dependent-cocone-sequential-diagram : + refl-htpy-dependent-cocone-sequential-diagram : ( d : dependent-cocone-sequential-diagram c P) → htpy-dependent-cocone-sequential-diagram P d d - pr1 (reflexive-htpy-dependent-cocone-sequential-diagram d) n = refl-htpy - pr2 (reflexive-htpy-dependent-cocone-sequential-diagram d) n = right-unit-htpy + pr1 (refl-htpy-dependent-cocone-sequential-diagram d) n = refl-htpy + pr2 (refl-htpy-dependent-cocone-sequential-diagram d) n = right-unit-htpy htpy-eq-dependent-cocone-sequential-diagram : ( d d' : dependent-cocone-sequential-diagram c P) → ( d ＝ d') → htpy-dependent-cocone-sequential-diagram P d d' htpy-eq-dependent-cocone-sequential-diagram d .d refl = - reflexive-htpy-dependent-cocone-sequential-diagram d + refl-htpy-dependent-cocone-sequential-diagram d abstract is-torsorial-htpy-dependent-cocone-sequential-diagram : diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md index e9c43a227c..6ca9d6998d 100644 --- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md @@ -228,15 +228,15 @@ module _ { l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2) where - reflexive-htpy-hom-sequential-diagram : + refl-htpy-hom-sequential-diagram : ( f : hom-sequential-diagram A B) → htpy-hom-sequential-diagram B f f - pr1 (reflexive-htpy-hom-sequential-diagram f) = ev-pair refl-htpy - pr2 (reflexive-htpy-hom-sequential-diagram f) = ev-pair right-unit-htpy + pr1 (refl-htpy-hom-sequential-diagram f) = ev-pair refl-htpy + pr2 (refl-htpy-hom-sequential-diagram f) = ev-pair right-unit-htpy htpy-eq-sequential-diagram : ( f f' : hom-sequential-diagram A B) → ( f ＝ f') → htpy-hom-sequential-diagram B f f' - htpy-eq-sequential-diagram f .f refl = reflexive-htpy-hom-sequential-diagram f + htpy-eq-sequential-diagram f .f refl = refl-htpy-hom-sequential-diagram f abstract is-torsorial-htpy-sequential-diagram :