From 53e8b15e09f1f7bc79e9b45af7c100ca9adfcf82 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 18 Oct 2023 00:49:38 +0200 Subject: [PATCH] make pre-commit --- .../natural-isomorphisms-functors-large-precategories.lagda.md | 2 +- ...tural-transformations-functors-large-precategories.lagda.md | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md b/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md index 81b5dcab44..edaf9fc991 100644 --- a/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md +++ b/src/category-theory/natural-isomorphisms-functors-large-precategories.lagda.md @@ -66,7 +66,7 @@ module _ ( hom-iso-Large-Precategory D ( iso-natural-isomorphism-Large-Precategory Y)) ( hom-functor-Large-Precategory G f) - + open natural-isomorphism-Large-Precategory public natural-transformation-natural-isomorphism-Large-Precategory : diff --git a/src/category-theory/natural-transformations-functors-large-precategories.lagda.md b/src/category-theory/natural-transformations-functors-large-precategories.lagda.md index a1be0c3454..40e89cd14c 100644 --- a/src/category-theory/natural-transformations-functors-large-precategories.lagda.md +++ b/src/category-theory/natural-transformations-functors-large-precategories.lagda.md @@ -59,7 +59,7 @@ module _ ( τ X) ( τ Y) ( hom-functor-Large-Precategory G f) - + record natural-transformation-Large-Precategory : UUω where constructor make-natural-transformation @@ -102,7 +102,6 @@ module _ ( inv ( left-unit-law-comp-hom-Large-Precategory D ( hom-functor-Large-Precategory F f))) - id-natural-transformation-Large-Precategory : natural-transformation-Large-Precategory C D F F