Categorical bits and pieces (#1008)

* Make the Yoneda embedding more universe polymorphic

* Make isEquivalence an actual hprop.

* Fix uses of isEquivalence for now proper definition.

* Refactor slice category and add new properties.

* More properties of mono/epi-morphisms.

* Separate triangle identities from Adjoint record.

* Add forgetΣPropCat functor.

* Use common definition of representable presheaves for Yoneda.

This has the same computational behavior, except that you get more definitional
equalities since functors don't have eta-expansion.

* Faithful functors reflect monos.

* Add adjoint equivalences.

* Add category of subobjects.

Cubical/Categories/Adjoint.agda

@@ -41,19 +41,25 @@ definition, followed by the natural bijection
 definition.
 -}
 
-module UnitCounit where
+module UnitCounit {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
+  record TriangleIdentities
+    (η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
+    (ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
+    : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+    where
+    field
+      Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
+      Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id
 
   -- Adjoint def 1: unit-counit
-  record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C)
-                  : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+  record _⊣_ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
     field
       -- unit
       η : 𝟙⟨ C ⟩ ⇒ (funcComp G F)
       -- counit
       ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩
-      -- triangle identities
-      Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
-      Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id
+      triangleIdentities : TriangleIdentities η ε
+    open TriangleIdentities triangleIdentities public
 
 module NaturalBijection where
   -- Adjoint def 2: natural bijection
@@ -164,8 +170,9 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (
     adj'→adj = record
       { η = η'
       ; ε = ε'
-      ; Δ₁ = Δ₁'
-      ; Δ₂ = Δ₂' }
+      ; triangleIdentities = record
+        {Δ₁ = Δ₁'
+        ; Δ₂ = Δ₂' }}
 
       where
         -- ETA

Cubical/Categories/Constructions/Elements.agda

@@ -13,7 +13,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
 
 import Cubical.Categories.Morphism as Morphism
-import Cubical.Categories.Constructions.Slice as Slice
+import Cubical.Categories.Constructions.Slice.Base as Slice
 
 -- some issues
 -- * always need to specify objects during composition because can't infer isSet