corrections

trees/agda-0005.tree

@@ -1,11 +1,11 @@
 \taxon{formalization}
 \author{fredrik-bakke}
-\title{Wild #{(\infty,\infty)}-categories}
+\title{Wild higher categories}
 \meta{external}{https://unimath.github.io/agda-unimath/wild-category-theory.html}
 \meta{status}{on the shelf}
 
 \p{
-  We can utilize parts of #{(\infty,\infty)}-category theory in univalent type theory using a globular model.
+  We can utilize parts of higher category theory in univalent type theory using a globular model.
   [agda-unimath#1099](https://github.com/UniMath/agda-unimath/pull/1099)
   This is a collaborative effort together with [[vojtech-stepancik]].
 }

trees/common.tree

@@ -17,6 +17,16 @@
   }
 }
 
+\def\question[body]{
+  \scope{
+    \put\transclude/toc{false}
+    \subtree{
+      \taxon{question}
+      \body
+    }
+  }
+}
+
 \def\proof[body]{
   \scope{
     \put\transclude/toc{false}
@@ -107,7 +117,8 @@
 \def\unit-type{#{\textbf{1}}}
 \def\bool-type{#{\textbf{2}}}
 \def\directed-interval{#{𝟚}}
-\def\sphere-type{#{\mathbb{S}}}
+\def\sphere{#{\mathbb{S}}}
+\def\directed-sphere{#{{\vec{\sphere}}}}
 \def\bN{#{\mathbb{N}}}
 
 \def\jdgeq{#{\equiv}}
@@ -124,7 +135,10 @@
 \def\po{{#{⌜}}}
 
 \def\hom-map{#{\mathop{\texttt{hom-map}}}}
+\def\spine[dimension]{#{\mathop{\texttt{spine}}{\dimension}}}
 \def\ap{#{\mathop{\texttt{ap}}}}
+\def\pr{#{\mathop{\texttt{pr}}}}
+\def\directed-suspension{#{\mathop{\vec{\Sigma}}}}
 \def\point{#{\mathop{\texttt{point}}}}
 \def\rec{#{\mathop{\texttt{rec}}}}
 \def\ind{#{\mathop{\texttt{ind}}}}
@@ -136,6 +150,10 @@
 \def\fiberwise-orthogonal{#{\mathrel{\perp^\mathrm{f}}}}
 
 \def\Hom{#{\textrm{Hom}}}
+\def\Set{#{\textrm{Set}}}
+\def\Prop{#{\textrm{Prop}}}
+\def\Space{#{\textrm{S}}}
+\def\op[x]{#{{\x}^{\textrm{op}}}}
 \def\simplex-category{#{\mathbf{\Delta}}}
 
 

trees/fb-0001.tree

@@ -9,6 +9,11 @@
   This is my personal page where I manage my personal notes as well as miscellaneous exposition related to my work. The web page is written using [Forester](https://www.jonmsterling.com/jms-005P.xml).
 }
 
+\p{
+   Please keep in mind that this web page is in early development and is thus largely incomplete and may be subject to big changes in the future.
+}
+
+
 \scope{
 \transclude{fb-0002}
 \transclude{fb-0003}

trees/fb-0004.tree

@@ -1,6 +1,6 @@
 \taxon{lecture note}
 \title{Segal spaces in Homotopy Type Theory}
-\date{2024-05-15}
+\date{2024-05-16}
 \author{fredrik-bakke}
 \import{common}
 \meta{venue}{FMF, University of Ljubljana}

trees/hott-000G.tree

@@ -17,7 +17,7 @@
       The unique lifting condition asks that there, for every element #{y : Y} exists a unique #{x :  X} such that #{g(x) = y}. In other words, the fibers of #{g} must be contractible.
     }
     \li{
-      More generally, a map is #{n}-truncated iff it is #{(\sphere-type^{n+1}\to \unit-type)}-orthogonal.
+      More generally, a map is #{n}-truncated iff it is #{(\sphere^{n+1}\to \unit-type)}-orthogonal.
     }
   }
 }

trees/hott-000H.tree

@@ -9,7 +9,7 @@
       Equivalences are orthogonal to every map, so every map is #{(\empty-type \to \unit-type)}-anodyne.
     }
     \li{
-      #{(n+1)}-truncated maps are also #{n}-truncated, so the map #{(\sphere-type^n\to \unit-type)} is #{(\sphere-type^{n-1}\to \unit-type)}-anodyne.
+      #{(n+1)}-truncated maps are also #{n}-truncated, so the map #{(\sphere^n\to \unit-type)} is #{(\sphere^{n-1}\to \unit-type)}-anodyne.
     }
   }
 }

trees/stt-000E.tree

@@ -4,6 +4,6 @@
 \import{common}
 
 \transclude{stt-000F}
-\transclude{stt-000G}
 \transclude{stt-000H}
+\transclude{stt-000G}
 \transclude{stt-000K}

trees/stt-000G.tree

@@ -6,13 +6,14 @@
 \p{
   Let #{A} be a Segal type and let every type labelled with a "#{B}" be Segal. Then the following types are also Segal
   \ol{
-    \li{Retracts of Segal types}
-    \li{#{\sigma-type{a : A}B(a)}}
+    \li{Retracts of #{A}}
     \li{#{\pi-type{i : I}B(i)}}
     \li{#{I \to B}}
     \li{#{B_1 \times B_2}}
     \li{#{B_1 \times_A B_2}}
-    \li{#{\lim_{(n:\bN)} B_n}}
+    \li{#{\lim_{(n:\bN)} B_n}}.
   }
+
+  Moreover, if #{B} is an inner family over #{A}, then #{\sigma-type{x:A}B(x)} is Segal.
 }
 \proof{Follows by [[hott-0004]].}