chore: rexport Displayed from Displayed.Reasoning

TOTBWF · plt-amy · commit 10f5dde59aa2 · 2023-08-01T21:25:44.000-03:00
diff --git a/src/Cat/Displayed/Cartesian.lagda.md b/src/Cat/Displayed/Cartesian.lagda.md
@@ -3,7 +3,7 @@
 open import Cat.Displayed.Base
 open import Cat.Prelude
 
-import Cat.Displayed.Reasoning as DR
+import Cat.Displayed.Reasoning
 import Cat.Displayed.Morphism
 import Cat.Reasoning
 ```
@@ -13,11 +13,15 @@ import Cat.Reasoning
 module Cat.Displayed.Cartesian
   {o ℓ o′ ℓ′} {B : Precategory o ℓ} (E : Displayed B o′ ℓ′) where
 
+```
+
+<!--
+```agda
 open Cat.Reasoning B
-open Displayed E
+open Cat.Displayed.Reasoning E
 open Cat.Displayed.Morphism E
-open DR E
 ```
+-->
 
 # Cartesian morphisms and Fibrations
 
diff --git a/src/Cat/Displayed/Cartesian/Identity.lagda.md b/src/Cat/Displayed/Cartesian/Identity.lagda.md
@@ -33,7 +33,6 @@ private
 open Cat.Displayed.Univalence.Reasoning E
 open Cat.Displayed.Univalence E
 open Cat.Displayed.Morphism E
-open Displayed E
 open Dr E
 open _≅[_]_
 ```
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -30,7 +30,6 @@ open Cartesian-fibration cartesian
 open Cat.Displayed.Reasoning E
 open Cat.Reasoning B
 open Cartesian-lift
-open Displayed E
 open is-cartesian
 open Functor
 ```
diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md
@@ -24,7 +24,6 @@ module Cat.Displayed.Cartesian.Right
   where
 
 open Cat.Reasoning ℬ
-open Displayed ℰ
 open Cat.Displayed.Cartesian ℰ
 open Cat.Displayed.Morphism ℰ
 open Cat.Displayed.Reasoning ℰ
diff --git a/src/Cat/Displayed/Cartesian/Weak.lagda.md b/src/Cat/Displayed/Cartesian/Weak.lagda.md
@@ -31,7 +31,6 @@ module Cat.Displayed.Cartesian.Weak
 <!--
 ```agda
 open CR ℬ
-open Displayed ℰ
 open Cart ℰ
 open DR ℰ
 open DM ℰ
diff --git a/src/Cat/Displayed/Cocartesian.lagda.md b/src/Cat/Displayed/Cocartesian.lagda.md
@@ -17,7 +17,6 @@ module Cat.Displayed.Cocartesian
   {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where
 
 open Cat.Reasoning ℬ
-open Displayed ℰ
 open Cat.Displayed.Morphism ℰ
 open Cat.Displayed.Morphism.Duality ℰ
 open DR ℰ
diff --git a/src/Cat/Displayed/Cocartesian/Indexing.lagda.md b/src/Cat/Displayed/Cocartesian/Indexing.lagda.md
@@ -22,7 +22,6 @@ module Cat.Displayed.Cocartesian.Indexing
 <!--
 ```agda
 open Cat.Reasoning ℬ
-open Displayed ℰ
 open Cat.Displayed.Reasoning ℰ
 open Cocartesian-fibration opfibration
 open Functor
diff --git a/src/Cat/Displayed/Cocartesian/Weak.lagda.md b/src/Cat/Displayed/Cocartesian/Weak.lagda.md
@@ -32,7 +32,6 @@ module Cat.Displayed.Cocartesian.Weak
 <!--
 ```agda
 open CR ℬ
-open Displayed ℰ
 open Cocart ℰ
 open Cat.Displayed.Morphism ℰ
 open Cat.Displayed.Morphism.Duality ℰ
diff --git a/src/Cat/Displayed/Fibre.lagda.md b/src/Cat/Displayed/Fibre.lagda.md
@@ -15,7 +15,6 @@ module Cat.Displayed.Fibre
   (E : Displayed B o′ ℓ′)
   where
 
-open Displayed E
 open Ds
 open Dr E
 open Cr B
diff --git a/src/Cat/Displayed/Instances/Diagrams.lagda.md b/src/Cat/Displayed/Instances/Diagrams.lagda.md
@@ -24,7 +24,6 @@ module Cat.Displayed.Instances.Diagrams
   where
 
 open Cat.Reasoning B
-open Displayed E
 open Cat.Displayed.Reasoning E
 open Functor
 open _=>_
diff --git a/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md b/src/Cat/Displayed/Instances/DisplayedFamilies.lagda.md
@@ -25,7 +25,6 @@ module Cat.Displayed.Instances.DisplayedFamilies
 <!--
 ```agda
 open Cat.Reasoning B
-open Displayed E
 open Cat.Displayed.Reasoning E
 open Functor
 
diff --git a/src/Cat/Displayed/Instances/Lifting.lagda.md b/src/Cat/Displayed/Instances/Lifting.lagda.md
@@ -61,7 +61,6 @@ module _
   private module J = Precategory J
 
   open Cat.Reasoning B
-  open Displayed E
   open Cat.Displayed.Reasoning E
 ```
 -->
@@ -164,7 +163,6 @@ module _
   private module J = Precategory J
 
   open Cat.Reasoning B
-  open Displayed E
   open Cat.Displayed.Reasoning E
   open Lifting
 ```
@@ -308,7 +306,6 @@ module _
   private module J = Precategory J
 
   open Cat.Reasoning B
-  open Displayed E
   open Cat.Displayed.Reasoning E
   open Lifting
   open _=[_]=>l_
diff --git a/src/Cat/Displayed/InternalSum.lagda.md b/src/Cat/Displayed/InternalSum.lagda.md
@@ -43,5 +43,5 @@ record Internal-sum : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)
   no-eta-equality
   field
     ∐ : Vertical-fibred-functor (Disp-family E) E
-    adjunction : ∐ ⊣↓ ConstDispFamVf E
+    adjunction : ∐ ⊣f↓ ConstDispFamVf E
 ```
diff --git a/src/Cat/Displayed/Morphism.lagda.md b/src/Cat/Displayed/Morphism.lagda.md
@@ -18,7 +18,6 @@ module Cat.Displayed.Morphism
 
 <!--
 ```agda
-open Displayed ℰ
 open Cat.Reasoning ℬ
 open Cat.Displayed.Reasoning ℰ
 private variable
diff --git a/src/Cat/Displayed/Morphism/Duality.lagda.md b/src/Cat/Displayed/Morphism/Duality.lagda.md
@@ -27,7 +27,6 @@ private
   module ℰ = Cat.Displayed.Morphism ℰ
   module ℰ^op = Cat.Displayed.Morphism (ℰ ^total-op)
 
-  open Displayed ℰ
   open Cat.Morphism.Duality ℬ
   open Cat.Displayed.Reasoning ℰ
 
diff --git a/src/Cat/Displayed/Reasoning.lagda.md b/src/Cat/Displayed/Reasoning.lagda.md
diff --git a/src/Cat/Displayed/Solver.agda b/src/Cat/Displayed/Solver.agda
diff --git a/src/Cat/Displayed/Univalence/Reasoning.lagda.md b/src/Cat/Displayed/Univalence/Reasoning.lagda.md
diff --git a/src/Cat/Functor/Hom/Displayed.lagda.md b/src/Cat/Functor/Hom/Displayed.lagda.md
