universal property isomorphisms

src/globular-types/binary-globular-maps.lagda.md

@@ -13,6 +13,7 @@ open import foundation.universe-levels
 
 open import globular-types.globular-maps
 open import globular-types.globular-types
+open import globular-types.points-globular-types
 ```
 
 </details>
@@ -98,3 +99,29 @@ module _
       ( 1-cell-binary-globular-map-binary-globular-map
         ( 1-cell-binary-globular-map-binary-globular-map F))
 ```
+
+### Evaluating one of the arguments of a binary globular map
+
+```agda
+ev-left-binary-globular-map :
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {G : Globular-Type l1 l2} {H : Globular-Type l3 l4} {K : Globular-Type l5 l6}
+  (F : binary-globular-map G H K) (x : point-Globular-Type G) → globular-map H K
+0-cell-globular-map (ev-left-binary-globular-map F x) =
+  0-cell-binary-globular-map F (0-cell-point-Globular-Type x)
+1-cell-globular-map-globular-map (ev-left-binary-globular-map F x) =
+  ev-left-binary-globular-map
+    ( 1-cell-binary-globular-map-binary-globular-map F)
+    ( 1-cell-point-point-Globular-Type x)
+
+ev-right-binary-globular-map :
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {G : Globular-Type l1 l2} {H : Globular-Type l3 l4} {K : Globular-Type l5 l6}
+  (F : binary-globular-map G H K) (x : point-Globular-Type H) → globular-map G K
+0-cell-globular-map (ev-right-binary-globular-map F x) y =
+  0-cell-binary-globular-map F y (0-cell-point-Globular-Type x)
+1-cell-globular-map-globular-map (ev-right-binary-globular-map F x) =
+  ev-right-binary-globular-map
+    ( 1-cell-binary-globular-map-binary-globular-map F)
+    ( 1-cell-point-point-Globular-Type x)
+```

src/globular-types/globular-equivalences.lagda.md

@@ -29,47 +29,90 @@ A {{#concept "globular equivalence" Agda=globular-equiv}} `e` between
 pair of $n$-cells `x` and `y`, an equivalence of $(n+1)$-cells
 
 ```text
-  eₙ₊₁ : (𝑛+1)-Cell A x y ≃ (𝑛+1)-Cell B (eₙ x) (eₙ y).
+  eₙ₊₁ : Aₙ₊₁ x y ≃ Bₙ₊₁ (eₙ x) (eₙ y).
 ```
 
 ## Definitions
 
-### Equivalences between globular types
+### The predicate on a globular map of being an equivalence
 
 ```agda
 record
-  globular-equiv
-    {l1 l2 l3 l4 : Level} (A : Globular-Type l1 l2) (B : Globular-Type l3 l4) :
+  is-equiv-globular-map
+    {l1 l2 l3 l4 : Level}
+    {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
+    (f : globular-map A B) :
     UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   where
   coinductive
 
   field
-    0-cell-equiv-globular-equiv :
-      0-cell-Globular-Type A ≃ 0-cell-Globular-Type B
-
-  0-cell-globular-equiv : 0-cell-Globular-Type A → 0-cell-Globular-Type B
-  0-cell-globular-equiv = map-equiv 0-cell-equiv-globular-equiv
+    is-equiv-0-cell-is-equiv-globular-map : is-equiv (0-cell-globular-map f)
 
-  field
-    1-cell-globular-equiv-globular-equiv :
+    1-cell-is-equiv-globular-map :
       {x y : 0-cell-Globular-Type A} →
-      globular-equiv
-        ( 1-cell-globular-type-Globular-Type A x y)
-        ( 1-cell-globular-type-Globular-Type B
-          ( 0-cell-globular-equiv x)
-          ( 0-cell-globular-equiv y))
+      is-equiv-globular-map (1-cell-globular-map-globular-map f {x} {y})
+
+open is-equiv-globular-map public
+```
 
-open globular-equiv public
+### Equivalences between globular types
 
-globular-map-globular-equiv :
-  {l1 l2 l3 l4 : Level}
-  {A : Globular-Type l1 l2} {B : Globular-Type l3 l4} →
-  globular-equiv A B → globular-map A B
-0-cell-globular-map (globular-map-globular-equiv e) =
-  map-equiv (0-cell-equiv-globular-equiv e)
-1-cell-globular-map-globular-map (globular-map-globular-equiv e) =
-  globular-map-globular-equiv (1-cell-globular-equiv-globular-equiv e)
+```agda
+globular-equiv :
+  {l1 l2 l3 l4 : Level} → Globular-Type l1 l2 → Globular-Type l3 l4 →
+  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+globular-equiv A B = Σ (globular-map A B) (is-equiv-globular-map)
+
+module _
+  {l1 l2 l3 l4 : Level} {A : Globular-Type l1 l2} {B : Globular-Type l3 l4}
+  (e : globular-equiv A B)
+  where
+
+  globular-map-globular-equiv : globular-map A B
+  globular-map-globular-equiv = pr1 e
+
+  is-equiv-globular-equiv : is-equiv-globular-map globular-map-globular-equiv
+  is-equiv-globular-equiv = pr2 e
+
+  0-cell-map-globular-equiv : 0-cell-Globular-Type A → 0-cell-Globular-Type B
+  0-cell-map-globular-equiv =
+    0-cell-globular-map globular-map-globular-equiv
+
+  is-equiv-0-cell-map-globular-equiv : is-equiv 0-cell-map-globular-equiv
+  is-equiv-0-cell-map-globular-equiv =
+    is-equiv-0-cell-is-equiv-globular-map is-equiv-globular-equiv
+
+  0-cell-globular-equiv : 0-cell-Globular-Type A ≃ 0-cell-Globular-Type B
+  0-cell-globular-equiv =
+    0-cell-map-globular-equiv , is-equiv-0-cell-map-globular-equiv
+
+  1-cell-globular-map-globular-equiv :
+    (x y : 0-cell-Globular-Type A) →
+    globular-map
+      ( 1-cell-globular-type-Globular-Type A x y)
+      ( 1-cell-globular-type-Globular-Type B
+        ( 0-cell-map-globular-equiv x)
+        ( 0-cell-map-globular-equiv y))
+  1-cell-globular-map-globular-equiv x y =
+    1-cell-globular-map-globular-map globular-map-globular-equiv
+
+  is-equiv-1-cell-globular-map-globular-equiv :
+    {x y : 0-cell-Globular-Type A} →
+    is-equiv-globular-map (1-cell-globular-map-globular-equiv x y)
+  is-equiv-1-cell-globular-map-globular-equiv =
+    1-cell-is-equiv-globular-map is-equiv-globular-equiv
+
+  1-cell-globular-equiv-globular-equiv :
+    {x y : 0-cell-Globular-Type A} →
+    globular-equiv
+      ( 1-cell-globular-type-Globular-Type A x y)
+      ( 1-cell-globular-type-Globular-Type B
+        ( 0-cell-map-globular-equiv x)
+        ( 0-cell-map-globular-equiv y))
+  1-cell-globular-equiv-globular-equiv {x} {y} =
+    1-cell-globular-map-globular-equiv x y ,
+    is-equiv-1-cell-globular-map-globular-equiv
 
 module _
   {l1 l2 l3 l4 : Level}
@@ -81,20 +124,19 @@ module _
     {x y : 0-cell-Globular-Type A} →
     1-cell-Globular-Type A x y ≃
     1-cell-Globular-Type B
-      ( 0-cell-globular-equiv e x)
-      ( 0-cell-globular-equiv e y)
+      ( 0-cell-map-globular-equiv e x)
+      ( 0-cell-map-globular-equiv e y)
   1-cell-equiv-globular-equiv =
-    0-cell-equiv-globular-equiv
-      ( 1-cell-globular-equiv-globular-equiv e)
+    0-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e)
 
-  1-cell-globular-equiv :
+  1-cell-map-globular-equiv :
     {x y : 0-cell-Globular-Type A} →
     1-cell-Globular-Type A x y →
     1-cell-Globular-Type B
-      ( 0-cell-globular-equiv e x)
-      ( 0-cell-globular-equiv e y)
-  1-cell-globular-equiv =
-    0-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e)
+      ( 0-cell-map-globular-equiv e x)
+      ( 0-cell-map-globular-equiv e y)
+  1-cell-map-globular-equiv =
+    0-cell-map-globular-equiv (1-cell-globular-equiv-globular-equiv e)
 
 module _
   {l1 l2 l3 l4 : Level}
@@ -107,8 +149,8 @@ module _
     {f g : 1-cell-Globular-Type A x y} →
     2-cell-Globular-Type A f g ≃
     2-cell-Globular-Type B
-      ( 1-cell-globular-equiv e f)
-      ( 1-cell-globular-equiv e g)
+      ( 1-cell-map-globular-equiv e f)
+      ( 1-cell-map-globular-equiv e g)
   2-cell-equiv-globular-equiv =
     1-cell-equiv-globular-equiv
       ( 1-cell-globular-equiv-globular-equiv e)
@@ -118,10 +160,10 @@ module _
     {f g : 1-cell-Globular-Type A x y} →
     2-cell-Globular-Type A f g →
     2-cell-Globular-Type B
-      ( 1-cell-globular-equiv e f)
-      ( 1-cell-globular-equiv e g)
+      ( 1-cell-map-globular-equiv e f)
+      ( 1-cell-map-globular-equiv e g)
   2-cell-globular-equiv =
-    1-cell-globular-equiv (1-cell-globular-equiv-globular-equiv e)
+    1-cell-map-globular-equiv (1-cell-globular-equiv-globular-equiv e)
 
 module _
   {l1 l2 l3 l4 : Level}
@@ -145,30 +187,51 @@ module _
 ### The identity equivalence on a globular type
 
 ```agda
+is-equiv-id-globular-map :
+  {l1 l2 : Level} (A : Globular-Type l1 l2) →
+  is-equiv-globular-map (id-globular-map A)
+is-equiv-0-cell-is-equiv-globular-map (is-equiv-id-globular-map A) = is-equiv-id
+1-cell-is-equiv-globular-map (is-equiv-id-globular-map A) =
+  is-equiv-id-globular-map (1-cell-globular-type-Globular-Type A _ _)
+
 id-globular-equiv :
   {l1 l2 : Level} (A : Globular-Type l1 l2) → globular-equiv A A
-id-globular-equiv A =
-  λ where
-  .0-cell-equiv-globular-equiv → id-equiv
-  .1-cell-globular-equiv-globular-equiv {x} {y} →
-    id-globular-equiv (1-cell-globular-type-Globular-Type A x y)
+id-globular-equiv A = id-globular-map A , is-equiv-id-globular-map A
 ```
 
 ### Composition of equivalences of globular types
 
 ```agda
+is-equiv-comp-globular-map :
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : Globular-Type l1 l2}
+  {B : Globular-Type l3 l4}
+  {C : Globular-Type l5 l6}
+  {g : globular-map B C}
+  {f : globular-map A B} →
+  is-equiv-globular-map g →
+  is-equiv-globular-map f →
+  is-equiv-globular-map (comp-globular-map g f)
+is-equiv-0-cell-is-equiv-globular-map (is-equiv-comp-globular-map G F) =
+  is-equiv-comp _ _
+    ( is-equiv-0-cell-is-equiv-globular-map F)
+    ( is-equiv-0-cell-is-equiv-globular-map G)
+1-cell-is-equiv-globular-map (is-equiv-comp-globular-map G F) =
+  is-equiv-comp-globular-map
+    ( 1-cell-is-equiv-globular-map G)
+    ( 1-cell-is-equiv-globular-map F)
+
 comp-globular-equiv :
   {l1 l2 l3 l4 l5 l6 : Level}
   {A : Globular-Type l1 l2}
   {B : Globular-Type l3 l4}
   {C : Globular-Type l5 l6} →
   globular-equiv B C → globular-equiv A B → globular-equiv A C
 comp-globular-equiv g f =
-  λ where
-  .0-cell-equiv-globular-equiv →
-    0-cell-equiv-globular-equiv g ∘e 0-cell-equiv-globular-equiv f
-  .1-cell-globular-equiv-globular-equiv →
-    comp-globular-equiv
-      ( 1-cell-globular-equiv-globular-equiv g)
-      ( 1-cell-globular-equiv-globular-equiv f)
+  comp-globular-map
+    ( globular-map-globular-equiv g)
+    ( globular-map-globular-equiv f) ,
+  is-equiv-comp-globular-map
+    ( is-equiv-globular-equiv g)
+    ( is-equiv-globular-equiv f)
 ```

src/globular-types/globular-maps.lagda.md

@@ -157,3 +157,8 @@ comp-globular-map g f =
       ( 1-cell-globular-map-globular-map g)
       ( 1-cell-globular-map-globular-map f)
 ```
+
+## See also
+
+- The dependent counterpart to globular maps is
+  [sections of dependent globular types](type-theories.sections-dependent-globular-types.md)

src/globular-types/reflexive-globular-equivalences.lagda.md

@@ -72,12 +72,12 @@ record
   0-cell-equiv-reflexive-globular-equiv :
     0-cell-Reflexive-Globular-Type G ≃ 0-cell-Reflexive-Globular-Type H
   0-cell-equiv-reflexive-globular-equiv =
-    0-cell-equiv-globular-equiv globular-equiv-reflexive-globular-equiv
+    0-cell-globular-equiv globular-equiv-reflexive-globular-equiv
 
   0-cell-reflexive-globular-equiv :
     0-cell-Reflexive-Globular-Type G → 0-cell-Reflexive-Globular-Type H
   0-cell-reflexive-globular-equiv =
-    0-cell-globular-equiv globular-equiv-reflexive-globular-equiv
+    0-cell-map-globular-equiv globular-equiv-reflexive-globular-equiv
 
   1-cell-equiv-reflexive-globular-equiv :
     {x y : 0-cell-Reflexive-Globular-Type G} →
@@ -95,7 +95,7 @@ record
       ( 0-cell-reflexive-globular-equiv x)
       ( 0-cell-reflexive-globular-equiv y)
   1-cell-reflexive-globular-equiv =
-    1-cell-globular-equiv globular-equiv-reflexive-globular-equiv
+    1-cell-map-globular-equiv globular-equiv-reflexive-globular-equiv
 
   1-cell-globular-equiv-reflexive-globular-equiv :
     {x y : 0-cell-Reflexive-Globular-Type G} →

src/wild-category-theory.lagda.md

@@ -18,7 +18,12 @@ open import wild-category-theory.colax-functors-noncoherent-wild-higher-precateg
 open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories public
 open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories public
 open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories public
+open import wild-category-theory.maps-noncoherent-omega-semiprecategories public
 open import wild-category-theory.maps-noncoherent-wild-higher-precategories public
 open import wild-category-theory.noncoherent-large-wild-higher-precategories public
+open import wild-category-theory.noncoherent-omega-semiprecategories public
 open import wild-category-theory.noncoherent-wild-higher-precategories public
+open import wild-category-theory.postcomposition-morphisms-noncoherent-omega-semiprecategories public
+open import wild-category-theory.precomposition-morphisms-noncoherent-omega-semiprecategories public
+open import wild-category-theory.universal-property-isomorphisms-noncoherent-omega-semiprecategories public
 ```