manage some unfinished work

UniMath · Oct 22, 2023 · 1e2b453 · 1e2b453
1 parent d66ecbf
commit 1e2b453
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 46 deletions.
diff --git a/src/category-theory/opposite-categories.lagda.md b/src/category-theory/opposite-categories.lagda.md
@@ -8,25 +8,15 @@ module category-theory.opposite-categories where
 
 ```agda
 open import category-theory.categories
-open import category-theory.composition-operations-on-binary-families-of-sets
-open import category-theory.isomorphisms-in-categories
-open import category-theory.isomorphisms-in-precategories
 open import category-theory.opposite-precategories
 open import category-theory.precategories
 
 open import foundation.dependent-pair-types
-open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
-open import foundation.function-extensionality
-open import foundation.function-types
-open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.involutions
-open import foundation.multivariable-homotopies
-open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
-open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 

diff --git a/src/category-theory/representable-functors-categories.lagda.md b/src/category-theory/representable-functors-categories.lagda.md
@@ -51,7 +51,7 @@ components `hom c x → hom b x` are defined by precomposition with `f`.
 
 ```agda
 representable-natural-transformation-Category :
-  {l1 l2 : Level} (C : Category l1 l2) (b c : obj-Category C)
+  {l1 l2 : Level} (C : Category l1 l2) {b c : obj-Category C}
   (f : hom-Category C b c) →
   natural-transformation-Category
     ( C)

diff --git a/src/category-theory/representable-functors-precategories.lagda.md b/src/category-theory/representable-functors-precategories.lagda.md
@@ -8,12 +8,10 @@ module category-theory.representable-functors-precategories where
 
 ```agda
 open import category-theory.functors-precategories
-open import category-theory.maps-from-small-to-large-precategories
 open import category-theory.maps-precategories
 open import category-theory.natural-transformations-functors-precategories
 open import category-theory.opposite-precategories
 open import category-theory.precategories
-open import category-theory.precategory-of-functors
 open import category-theory.presheaf-categories
 
 open import foundation.category-of-sets
@@ -149,15 +147,14 @@ module _
   pr2 map-representable-functor-copresheaf-Precategory =
     representable-natural-transformation-Precategory C
 
-  functor-representable-functor-copresheaf-Precategory :
-    functor-Precategory
-      ( opposite-Precategory C)
-      ( copresheaf-precategory-Large-Precategory C l2)
-  pr1 functor-representable-functor-copresheaf-Precategory =
-    representable-functor-Precategory C
-  pr1 (pr2 functor-representable-functor-copresheaf-Precategory) =
-    representable-natural-transformation-Precategory C
-  pr1 (pr2 (pr2 functor-representable-functor-copresheaf-Precategory)) =
-    {!   !}
-  pr2 (pr2 (pr2 functor-representable-functor-copresheaf-Precategory)) = {!   !}
+  -- functor-representable-functor-copresheaf-Precategory :
+  --   functor-Precategory
+  --     ( opposite-Precategory C)
+  --     ( copresheaf-precategory-Large-Precategory C l2)
+  -- pr1 functor-representable-functor-copresheaf-Precategory =
+  --   representable-functor-Precategory C
+  -- pr1 (pr2 functor-representable-functor-copresheaf-Precategory) =
+  --   representable-natural-transformation-Precategory C
+  -- pr1 (pr2 (pr2 functor-representable-functor-copresheaf-Precategory)) = {!   !}
+  -- pr2 (pr2 (pr2 functor-representable-functor-copresheaf-Precategory)) = {!   !}
 ```
diff --git a/src/category-theory/yoneda-lemma-categories.lagda.md b/src/category-theory/yoneda-lemma-categories.lagda.md
@@ -16,10 +16,7 @@ open import category-theory.representable-functors-categories
 open import category-theory.yoneda-lemma-precategories
 
 open import foundation.category-of-sets
-open import foundation.dependent-pair-types
 open import foundation.equivalences
-open import foundation.retractions
-open import foundation.sections
 open import foundation.sets
 open import foundation.universe-levels
 ```

diff --git a/src/category-theory/yoneda-lemma-precategories.lagda.md b/src/category-theory/yoneda-lemma-precategories.lagda.md
@@ -136,19 +136,6 @@ module _
     lemma-yoneda-Small-Large-Precategory
 ```
 
-### The yoneda embedding into the large category of sets
-
-#### Taking representable functors is a functor
-
-```agda
-module _
-  {l1 l2 l3 : Level} (C : Precategory l1 l2) (c : obj-Precategory C)
-  (F : functor-Small-Large-Precategory C Set-Large-Precategory l3)
-  where
-
-  map-yoneda-Small-Large-Precategory :
-```
-
 ## The yoneda lemma into the small category of sets
 
 ```agda

diff --git a/src/foundation/equality-dependent-function-types.lagda.md b/src/foundation/equality-dependent-function-types.lagda.md
@@ -15,7 +15,6 @@ open import foundation.universe-levels
 
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
-open import foundation-core.functoriality-dependent-function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.torsorial-type-families

diff --git a/src/foundation/multivariable-homotopies.lagda.md b/src/foundation/multivariable-homotopies.lagda.md
@@ -16,13 +16,8 @@ open import foundation.function-extensionality
 open import foundation.iterated-dependent-product-types
 open import foundation.universe-levels
 
-open import foundation-core.contractible-types
 open import foundation-core.functoriality-dependent-function-types
-open import foundation-core.homotopies
 open import foundation-core.identity-types
-open import foundation-core.propositions
-open import foundation-core.truncated-types
-open import foundation-core.truncation-levels
 ```
 
 </details>