Merge branch 'master' into universal-algebra

UniMath/Bicategories/DisplayedBicats/DisplayedUniversalArrow.v

@@ -197,14 +197,14 @@ Section MakeDisplayedLeftUniversalArrowIfPropositional.
                       (ff1 : xx -->[ f1] RR y yy) (ff2 : xx -->[ f2] RR y yy)
                       (α : f1 ==> f2),
               ff1 ==>[α] ff2
-              → (LL_mor x xx y yy f1 ff1) ==>[(# (right_adjoint ((pr22 LUR) x y)))%Cat α]
+              → (LL_mor x xx y yy f1 ff1) ==>[(# (right_adjoint ((pr22 LUR) x y)))%cat α]
                   (LL_mor x xx y yy f2 ff2)).
   Context (LL_unit : ∏ x xx y yy f ff,
               ff ==>[adjunit (adj x y) f]
-                (LL_mor x xx y yy (η x · (# R)%Cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))).
+                (LL_mor x xx y yy (η x · (# R)%cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))).
 
   Context (LL_unit_inv : ∏ x xx y yy f ff,
-        (LL_mor x xx y yy ((pr12 LUR) x · (# R)%Cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))
+        (LL_mor x xx y yy ((pr12 LUR) x · (# R)%cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))
           ==>[inv_from_z_iso (unit_pointwise_z_iso_from_adj_equivalence (adj x y) _)] ff).
 
   Context (LL_counit : ∏ x xx y yy f ff,
@@ -314,12 +314,12 @@ Section MakeDisplayedLeftUniversalArrowIfGroupoidalAndProp.
                       (ff1 : xx -->[ f1] RR y yy) (ff2 : xx -->[ f2] RR y yy)
                       (α : f1 ==> f2),
               ff1 ==>[α] ff2
-              → (LL_mor x xx y yy f1 ff1) ==>[(# (right_adjoint ((pr22 LUR) x y)))%Cat α]
+              → (LL_mor x xx y yy f1 ff1) ==>[(# (right_adjoint ((pr22 LUR) x y)))%cat α]
                   (LL_mor x xx y yy f2 ff2)
           ).
   Context (LL_unit : ∏ x xx y yy f ff,
         ff ==>[adjunit (adj x y) f]
-    (LL_mor x xx y yy (η x · (# R)%Cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))).
+    (LL_mor x xx y yy (η x · (# R)%cat f) (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR ff))).
 
   Context (LL_counit : ∏ x xx y yy f ff,
         (ηη x xx ;; disp_psfunctor_mor D1 D2 R RR (LL_mor x xx y yy f ff))

UniMath/CategoryTheory/Core/Categories.v

@@ -37,7 +37,6 @@ Definition precategory_morphisms { C : precategory_ob_mor } :
 
 Declare Scope cat.
 Delimit Scope cat with cat.     (* for precategories *)
-Delimit Scope cat with Cat.     (* a slight enhancement for categories *)
 Local Open Scope cat.
 
 Notation "a --> b" := (precategory_morphisms a b) : cat.

UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v

@@ -483,15 +483,15 @@ Section IsCartesianFromReindexDispCat.
             (identity _)
             (transportb
                (λ z, xx -->[ z] yy)
-               (id_left ((# F)%Cat f))
+               (id_left ((# F)%cat f))
                ff)
           ;;
           cartesian_factorisation
             Hff
             (identity _)
             (transportb
                (mor_disp (pr1 ℓ) yy)
-               (maponpaths (λ z, (# F)%Cat z) (id_left f))
+               (maponpaths (λ z, (# F)%cat z) (id_left f))
                (pr12 ℓ)))%mor_disp
       as m'.
     pose (@cartesian_factorisation_unique
@@ -530,7 +530,7 @@ Section IsCartesianFromReindexDispCat.
                 (identity _)
                 (transportb
                    (mor_disp (pr1 ℓ) yy)
-                   (maponpaths (λ z : C₁ ⟦ x, y ⟧, (# F)%Cat z) (id_left f))
+                   (maponpaths (λ z : C₁ ⟦ x, y ⟧, (# F) z) (id_left f))
                    (pr12 ℓ)))
           as q.
         cbn in q.
@@ -1120,7 +1120,7 @@ Section ReindexIsPB.
                 _
                 (pr2 (HD₂ _ _ (nat_z_iso_pointwise_z_iso α x) (pr2 (G x)))
                  ;;
-                 (pr2 (#G f))%Cat
+                 (pr2 (#G f))%cat
                  ;;
                  inv_mor_disp_from_z_iso
                    (pr2 (HD₂ _ _ (nat_z_iso_pointwise_z_iso α y) (pr2 (G y)))))%mor_disp).

UniMath/CategoryTheory/DisplayedCats/Functors.v

@@ -405,7 +405,7 @@ Section Disp_Functor.
                 {f : x --> y}
                 {xx : D₁ x}
                 {yy : D₁ y}
-                (ff : FF x xx -->[ (#F f)%Cat ] FF y yy)
+                (ff : FF x xx -->[ (#F f) ] FF y yy)
       : ♯FF (disp_functor_ff_inv FF HFF ff) = ff.
     Proof.
       apply (homotweqinvweq ((disp_functor_ff_weq FF HFF xx yy f))).

UniMath/CategoryTheory/DisplayedCats/Limits.v

@@ -401,7 +401,7 @@ Section fiber.
 
 End fiber.
 
-Check fiber_limit.
+(* Check fiber_limit. *)
 
 Definition fiber_limits
   {C : category}
@@ -464,7 +464,7 @@ Proof.
       intro j.
       set (RRt := make_LimCone _ _ _ RT1).
       set (RRtt := limArrowCommutes RRt x CC j).
-      set (RH := maponpaths (#π)%Cat RRtt).
+      set (RH := maponpaths (#π) RRtt).
       cbn in RH.
       apply RH.
     }

UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DispCatsEquivFunctors.v

@@ -167,7 +167,7 @@ Proof.
   - eapply pathscomp0.
     2: { apply pathsinv0. apply (transp_pres_comp' H_ob H'_ob H''_ob). }
     + eapply pathscomp0.
-      * exact (maponpaths (λ mor, mor · ((# F)%Cat g')) H_mor).
+      * exact (maponpaths (λ mor, mor · ((# F) g')) H_mor).
       * exact (maponpaths (λ mor, (transportf_mor H_ob H'_ob f) · mor) H'_mor).
 Defined.
 

UniMath/CategoryTheory/DisplayedCats/TotalAdjunction.v

@@ -168,7 +168,7 @@ Section TotalAdjunction.
          assert (hh : (# (left_functor F))
    (identity (pr1 x) · (η (pr1 x) · identity (right_functor F (left_functor F (pr1 x)))))
  · ε (left_functor F (pr1 x)) =
-                        (# (left_functor F))%Cat (adjunit F (pr1 x)) · adjcounit F (left_functor F (pr1 x))).
+                        (# (left_functor F)) (adjunit F (pr1 x)) · adjcounit F (left_functor F (pr1 x))).
          {
            apply maponpaths_2.
            apply maponpaths.
@@ -260,10 +260,10 @@ Section TotalAdjunction.
 
       assert (p : identity (right_functor F (pr1 x))
  · (η (right_functor F (pr1 x)) · identity (right_functor F (left_functor F (right_functor F (pr1 x)))))
- · (# (right_functor F))%Cat
+ · (# (right_functor F))
      (identity (left_functor F (right_functor F (pr1 x))) · (ε (pr1 x) · identity (pr1 x))) =
  unit_from_are_adjoints F (right_functor F (pr1 x))
-                        · (# (right_functor F))%Cat (counit_from_are_adjoints F (pr1 x))).
+                        · (# (right_functor F)) (counit_from_are_adjoints F (pr1 x))).
       {
         rewrite ! id_left.
         now rewrite ! id_right.
@@ -292,8 +292,8 @@ Section TotalAdjunction.
       assert (qq : identity (right_functor F (pr1 x))
  · (adjunit F (right_functor F (pr1 x))
     · identity (right_functor F (left_functor F (right_functor F (pr1 x)))))
- · (# (right_functor F))%Cat (adjcounit F (pr1 x)) =
-                    adjunit F (right_functor F (pr1 x)) · (# (right_functor F))%Cat (adjcounit F (pr1 x))).
+ · (# (right_functor F)) (adjcounit F (pr1 x)) =
+                    adjunit F (right_functor F (pr1 x)) · (# (right_functor F)) (adjcounit F (pr1 x))).
       {
         rewrite ! id_left.
         now rewrite ! id_right.

UniMath/CategoryTheory/FunctorCategory.v

@@ -612,8 +612,7 @@ Notation "[ C , D , hs ]" := (functor_precategory C D hs) : cat.
 
 Notation "[ C , D ]" := (functor_category C D) : cat.
 
-Declare Scope Cat.
-Notation "G □ F" := (functor_composite (F:[_,_]) (G:[_,_]) : [_,_]) (at level 35) : Cat.
+Notation "G □ F" := (functor_composite (F:[_,_]) (G:[_,_]) : [_,_]) (at level 35) : cat.
 (* to input: type "\Box" or "\square" or "\sqw" or "\sq" with Agda input method *)
 
 Definition functor_compose {A B C : category} (F : ob [A, B])

UniMath/CategoryTheory/Monoidal/Examples/MonoidalDialgebras.v

@@ -657,14 +657,14 @@ Section MonoidalNatTransToDialgebraLifting.
       use tpair.
       + cbn.
 
-        transparent assert (pfG_is_z_iso : (is_z_isomorphism ( (# G)%Cat (inv_from_z_iso (fmonoidal_preservestensordata Km x y,, fmonoidal_preservestensorstrongly (_,, pr2 Km) x y))))).
+        transparent assert (pfG_is_z_iso : (is_z_isomorphism ( (# G)%cat (inv_from_z_iso (fmonoidal_preservestensordata Km x y,, fmonoidal_preservestensorstrongly (_,, pr2 Km) x y))))).
         {
           use functor_on_is_z_isomorphism.
           apply is_z_iso_inv_from_z_iso.
         }
         use (z_iso_inv_to_right _ _ _ _ (_ ,, pfG_is_z_iso)).
 
-        transparent assert (pfF_is_z_iso : (is_z_isomorphism ((# F)%Cat
+        transparent assert (pfF_is_z_iso : (is_z_isomorphism ((# F)%cat
     (inv_from_z_iso
        (fmonoidal_preservestensordata Km x y,, fmonoidal_preservestensorstrongly (_,, pr2 Km) x y))))).
         {
@@ -681,7 +681,7 @@ Section MonoidalNatTransToDialgebraLifting.
       + cbn.
 
         transparent assert (pfL_is_z_iso :
-                             (is_z_isomorphism ( (# F)%Cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_ ,, pr2 Km)))))
+                             (is_z_isomorphism ( (# F)%cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_ ,, pr2 Km)))))
                            ).
         {
           use functor_on_is_z_isomorphism.
@@ -692,7 +692,7 @@ Section MonoidalNatTransToDialgebraLifting.
 
         transparent assert (pfR_is_z_iso
                              : (is_z_isomorphism
-                                  ((# G)%Cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_,, pr2 Km)))))).
+                                  ((# G)%cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_,, pr2 Km)))))).
         {
           use functor_on_is_z_isomorphism.
           apply is_z_iso_inv_from_z_iso.

UniMath/CategoryTheory/RepresentableFunctors/Representation.v

@@ -13,7 +13,6 @@ Require Import
         UniMath.CategoryTheory.RepresentableFunctors.Precategories.
 Require Import UniMath.MoreFoundations.Tactics.
 Local Open Scope cat.
-Local Open Scope Cat.
 
 Definition isUniversal {C:category} {X:[C^op,HSET]} {c:C} (x:c ⇒ X)
   := ∏ (c':C), isweq (λ f : c' --> c, x ⟲ f).

UniMath/Induction/W/Fibered.v

@@ -16,7 +16,7 @@ Require Import UniMath.Induction.FunctorAlgebras_legacy.
 Require Import UniMath.Induction.PolynomialFunctors.
 Require Import UniMath.Induction.W.Core.
 
-Local Open Scope Cat.
+Local Open Scope cat.
 
 Section Fibered.
   Context {A : UU} {B : A -> UU}.
@@ -52,7 +52,7 @@ Section Fibered.
     pose (supe := pr2 E).
     split with (∑ x : pr1 X, pr1 E x).
     intro z; cbn in z; unfold polynomial_functor_obj in *.
-    pose (z' := ((pr1 z),, pr1 ∘ (pr2 z)) : (∑ a : A, B a → pr1 X)).
+    pose (z' := ((pr1 z),, (pr1 ∘ (pr2 z))%functions) : (∑ a : A, B a → pr1 X)).
     refine (supx z',, supe z' (λ b, (pr2 (pr2 z b)))).
   Defined.
 
@@ -66,7 +66,7 @@ Section Fibered.
     pose (supx := pr2 X).
     pose (supe := pr2 E).
     exact ((∑ (f : ∏ x : pr1 X, pr1 E x),
-            ∏ a, f (supx a) = supe a (f ∘ (pr2 a)))).
+            ∏ a, f (supx a) = supe a (f ∘ (pr2 a))%functions)).
   Defined.
 
   (** A P-algebra section homotopy.
@@ -111,7 +111,7 @@ Section Fibered.
     - do 2 (apply maponpaths).
       unfold funhomotsec; cbn.
       assert (H : (λ x0 : B (pr1 x), idpath (pr1 f (pr2 x x0))) =
-                  (toforallpaths _ (pr1 f ∘ pr2 x) (pr1 f ∘ pr2 x) (idpath _))).
+                  (toforallpaths _ (pr1 f ∘ pr2 x)%functions (pr1 f ∘ pr2 x)%functions (idpath _))).
       reflexivity.
       refine ((maponpaths _ H) @ _).
       apply funextsec_toforallpaths.