fixup: actually get it compiling

the1lab · Aug 17, 2023 · 31218a6 · 31218a6
1 parent 5f3cf3c
commit 31218a6
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 2 deletions.
diff --git a/src/Cat/Diagram/Idempotent.lagda.md b/src/Cat/Diagram/Idempotent.lagda.md
@@ -58,11 +58,10 @@ is-split→is-idempotent {f = f} spl =
 
 It's not the case that idempotents are split in every category. Those
 where this is the case are called **idempotent-complete**. Every
-category can be embedded, by a [full and faithful] functor, into an
+category can be embedded, by a [[fully faithful]] functor, into an
 idempotent-complete category; This construction is called the [Karoubi
 envelope] of $\cC$.
 
-[full and faithful]: Cat.Functor.Properties.html#ff-functors
 [Karoubi envelope]: Cat.Instances.Karoubi.html
 
 ```agda

diff --git a/src/Cat/Displayed/Comprehension.lagda.md b/src/Cat/Displayed/Comprehension.lagda.md
@@ -27,6 +27,7 @@ module Cat.Displayed.Comprehension
 ```agda
 open Cat.Reasoning B
 open Cat.Displayed.Reasoning E
+open Displayed E
 open Functor
 open _=>_
 open Total-hom

diff --git a/src/Cat/Displayed/GenericObject.lagda.md b/src/Cat/Displayed/GenericObject.lagda.md
@@ -22,6 +22,7 @@ module Cat.Displayed.GenericObject
 open Precategory B
 open Cat.Displayed.Morphism E
 open Cat.Displayed.Reasoning E
+open Displayed E
 open Functor
 ```
 -->

diff --git a/src/Cat/Displayed/Univalence.lagda.md b/src/Cat/Displayed/Univalence.lagda.md
@@ -27,6 +27,7 @@ private
   module ∫E = Cat.Reasoning (∫ E)
   module E = Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
+open Displayed E
 open Total-hom
 open E
 ```

diff --git a/src/Cat/Displayed/Univalence/Reasoning.lagda.md b/src/Cat/Displayed/Univalence/Reasoning.lagda.md
@@ -36,6 +36,7 @@ private module B = Cr B
 open Cat.Displayed.Univalence E
 open Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
+open Displayed E
 open _≅[_]_
 ```
 -->