Deploying to gh-pages from @ 8ca88c6 🚀

hott/11-homotopy-pullbacks.rzk/index.html

@@ -1220,20 +1220,15 @@ <h3 id="interaction-with-horizontal-equivalences">Interaction with horizontal eq
 </span><span id="__span-4-24"><a id="__codelineno-4-24" name="__codelineno-4-24" href="#__codelineno-4-24"></a><span class="err">        </span><span class="p">( </span>Σ (a&#39; <span class="p">:</span><span class="err"> A&#39;), C (α a&#39;))</span>
 </span><span id="__span-4-25"><a id="__codelineno-4-25" name="__codelineno-4-25" href="#__codelineno-4-25"></a><span class="err">        ( total-type A C)</span>
 </span><span id="__span-4-26"><a id="__codelineno-4-26" name="__codelineno-4-26" href="#__codelineno-4-26"></a><span class="err">        ( total-map A&#39; C&#39; (</span><span class="p">\ </span>a&#39; <span class="err">→ C (α a&#39;)) γ)</span>
-</span><span id="__span-4-27"><a id="__codelineno-4-27" name="__codelineno-4-27" href="#__codelineno-4-27"></a><span class="err">        ( family-of-equiv-total-equiv</span>
-</span><span id="__span-4-28"><a id="__codelineno-4-28" name="__codelineno-4-28" href="#__codelineno-4-28"></a><span class="err">          ( A&#39; )</span>
-</span><span id="__span-4-29"><a id="__codelineno-4-29" name="__codelineno-4-29" href="#__codelineno-4-29"></a><span class="err">          ( C&#39; )</span>
-</span><span id="__span-4-30"><a id="__codelineno-4-30" name="__codelineno-4-30" href="#__codelineno-4-30"></a><span class="err">          ( </span><span class="p">\ </span>a&#39; <span class="err">→ C (α a&#39;) )</span>
-</span><span id="__span-4-31"><a id="__codelineno-4-31" name="__codelineno-4-31" href="#__codelineno-4-31"></a><span class="err">          ( γ)</span>
-</span><span id="__span-4-32"><a id="__codelineno-4-32" name="__codelineno-4-32" href="#__codelineno-4-32"></a><span class="err">          ( </span><span class="p">\ </span>a&#39; <span class="err">→ is-hc-α-γ a&#39;))</span>
-</span><span id="__span-4-33"><a id="__codelineno-4-33" name="__codelineno-4-33" href="#__codelineno-4-33"></a><span class="err">        ( \ (a&#39;, c) → (α a&#39;, c) )</span>
-</span><span id="__span-4-34"><a id="__codelineno-4-34" name="__codelineno-4-34" href="#__codelineno-4-34"></a><span class="err">        ( </span><span class="s">second</span>
-</span><span id="__span-4-35"><a id="__codelineno-4-35" name="__codelineno-4-35" href="#__codelineno-4-35"></a><span class="err">          ( total-equiv-pullback-is-equiv</span>
-</span><span id="__span-4-36"><a id="__codelineno-4-36" name="__codelineno-4-36" href="#__codelineno-4-36"></a><span class="err">            ( A&#39;)</span>
-</span><span id="__span-4-37"><a id="__codelineno-4-37" name="__codelineno-4-37" href="#__codelineno-4-37"></a><span class="err">            ( A )</span>
-</span><span id="__span-4-38"><a id="__codelineno-4-38" name="__codelineno-4-38" href="#__codelineno-4-38"></a><span class="err">            ( α )</span>
-</span><span id="__span-4-39"><a id="__codelineno-4-39" name="__codelineno-4-39" href="#__codelineno-4-39"></a><span class="err">            ( is-equiv-α )</span>
-</span><span id="__span-4-40"><a id="__codelineno-4-40" name="__codelineno-4-40" href="#__codelineno-4-40"></a><span class="err">            ( C ))))</span>
+</span><span id="__span-4-27"><a id="__codelineno-4-27" name="__codelineno-4-27" href="#__codelineno-4-27"></a><span class="err">        ( is-equiv-total-is-equiv-fiberwise A&#39; C&#39;</span>
+</span><span id="__span-4-28"><a id="__codelineno-4-28" name="__codelineno-4-28" href="#__codelineno-4-28"></a><span class="err">          ( </span><span class="p">\ </span>a&#39; <span class="err">→ C (α a&#39;) )</span>
+</span><span id="__span-4-29"><a id="__codelineno-4-29" name="__codelineno-4-29" href="#__codelineno-4-29"></a><span class="err">          ( γ)</span>
+</span><span id="__span-4-30"><a id="__codelineno-4-30" name="__codelineno-4-30" href="#__codelineno-4-30"></a><span class="err">          ( </span><span class="p">\ </span>a&#39; <span class="err">→ is-hc-α-γ a&#39;))</span>
+</span><span id="__span-4-31"><a id="__codelineno-4-31" name="__codelineno-4-31" href="#__codelineno-4-31"></a><span class="err">        ( \ (a&#39;, c) → (α a&#39;, c) )</span>
+</span><span id="__span-4-32"><a id="__codelineno-4-32" name="__codelineno-4-32" href="#__codelineno-4-32"></a><span class="err">        ( </span><span class="s">second</span>
+</span><span id="__span-4-33"><a id="__codelineno-4-33" name="__codelineno-4-33" href="#__codelineno-4-33"></a><span class="err">          ( equiv-total-pullback-is-equiv A&#39; A α</span>
+</span><span id="__span-4-34"><a id="__codelineno-4-34" name="__codelineno-4-34" href="#__codelineno-4-34"></a><span class="err">            ( is-equiv-α )</span>
+</span><span id="__span-4-35"><a id="__codelineno-4-35" name="__codelineno-4-35" href="#__codelineno-4-35"></a><span class="err">            ( C ))))</span>
 </span></code></pre></div>
 <p>Conversely, if both the upper and the lower maps are equivalences, then the
 square is homotopy-cartesian.</p>
@@ -1244,15 +1239,15 @@ <h3 id="interaction-with-horizontal-equivalences">Interaction with horizontal eq
 </span><span id="__span-5-5"><a id="__codelineno-5-5" name="__codelineno-5-5" href="#__codelineno-5-5"></a><span class="err">  )</span>
 </span><span id="__span-5-6"><a id="__codelineno-5-6" name="__codelineno-5-6" href="#__codelineno-5-6"></a><span class="err">  : is-homotopy-cartesian</span>
 </span><span id="__span-5-7"><a id="__codelineno-5-7" name="__codelineno-5-7" href="#__codelineno-5-7"></a><span class="err">  :=</span>
-</span><span id="__span-5-8"><a id="__codelineno-5-8" name="__codelineno-5-8" href="#__codelineno-5-8"></a><span class="err">    total-equiv-family-of-equiv</span>
-</span><span id="__span-5-9"><a id="__codelineno-5-9" name="__codelineno-5-9" href="#__codelineno-5-9"></a><span class="err">        A&#39; C&#39; ( </span><span class="p">\ </span>x <span class="err">→ C (α x) ) γ    </span><span class="c">-- use x instead of a&#39; to avoid shadowing</span>
+</span><span id="__span-5-8"><a id="__codelineno-5-8" name="__codelineno-5-8" href="#__codelineno-5-8"></a><span class="err">    is-equiv-fiberwise-is-equiv-total</span>
+</span><span id="__span-5-9"><a id="__codelineno-5-9" name="__codelineno-5-9" href="#__codelineno-5-9"></a><span class="err">        A&#39; C&#39; ( </span><span class="p">\ </span>x <span class="err">→ C (α x) ) γ</span>
 </span><span id="__span-5-10"><a id="__codelineno-5-10" name="__codelineno-5-10" href="#__codelineno-5-10"></a><span class="err">        ( is-equiv-right-factor</span>
 </span><span id="__span-5-11"><a id="__codelineno-5-11" name="__codelineno-5-11" href="#__codelineno-5-11"></a><span class="err">            ( total-type A&#39; C&#39;)</span>
 </span><span id="__span-5-12"><a id="__codelineno-5-12" name="__codelineno-5-12" href="#__codelineno-5-12"></a><span class="err">            </span><span class="p">( </span>Σ (x <span class="p">:</span><span class="err"> A&#39;), C (α x))</span>
 </span><span id="__span-5-13"><a id="__codelineno-5-13" name="__codelineno-5-13" href="#__codelineno-5-13"></a><span class="err">            ( total-type A C)</span>
 </span><span id="__span-5-14"><a id="__codelineno-5-14" name="__codelineno-5-14" href="#__codelineno-5-14"></a><span class="err">            ( total-map A&#39; C&#39; (</span><span class="p">\ </span>x <span class="err">→ C (α x)) γ)</span>
 </span><span id="__span-5-15"><a id="__codelineno-5-15" name="__codelineno-5-15" href="#__codelineno-5-15"></a><span class="err">            ( \ (x, c) → (α x, c) )</span>
-</span><span id="__span-5-16"><a id="__codelineno-5-16" name="__codelineno-5-16" href="#__codelineno-5-16"></a><span class="err">            ( </span><span class="s">second</span><span class="err"> ( total-equiv-pullback-is-equiv A&#39; A α is-equiv-α C))</span>
+</span><span id="__span-5-16"><a id="__codelineno-5-16" name="__codelineno-5-16" href="#__codelineno-5-16"></a><span class="err">            ( </span><span class="s">second</span><span class="err"> ( equiv-total-pullback-is-equiv A&#39; A α is-equiv-α C))</span>
 </span><span id="__span-5-17"><a id="__codelineno-5-17" name="__codelineno-5-17" href="#__codelineno-5-17"></a><span class="err">            ( is-equiv-homotopy</span>
 </span><span id="__span-5-18"><a id="__codelineno-5-18" name="__codelineno-5-18" href="#__codelineno-5-18"></a><span class="err">                ( total-type A&#39; C&#39;)</span>
 </span><span id="__span-5-19"><a id="__codelineno-5-19" name="__codelineno-5-19" href="#__codelineno-5-19"></a><span class="err">                ( total-type A C )</span>

simplicial-hott/03-extension-types.rzk/index.html

@@ -1851,7 +1851,7 @@ <h3 id="weak-extension-extensionality-implies-extension-extensionality">Weak ext
 </span><span id="__span-21-11"><a id="__codelineno-21-11" name="__codelineno-21-11" href="#__codelineno-21-11"></a><span class="err">        ( f = g)</span>
 </span><span id="__span-21-12"><a id="__codelineno-21-12" name="__codelineno-21-12" href="#__codelineno-21-12"></a><span class="err">        </span><span class="p">( </span>(t <span class="p">:</span><span class="err"> ψ ) → (f t = g t) [ϕ t ↦ </span><span class="s">refl</span><span class="err">])</span>
 </span><span id="__span-21-13"><a id="__codelineno-21-13" name="__codelineno-21-13" href="#__codelineno-21-13"></a><span class="err">        ( ext-htpy-eq I ψ ϕ A a f g)</span>
-</span><span id="__span-21-14"><a id="__codelineno-21-14" name="__codelineno-21-14" href="#__codelineno-21-14"></a><span class="err">  := total-equiv-family-of-equiv</span>
+</span><span id="__span-21-14"><a id="__codelineno-21-14" name="__codelineno-21-14" href="#__codelineno-21-14"></a><span class="err">  := is-equiv-fiberwise-is-equiv-total</span>
 </span><span id="__span-21-15"><a id="__codelineno-21-15" name="__codelineno-21-15" href="#__codelineno-21-15"></a><span class="err">      </span><span class="p">( </span>(t <span class="p">:</span><span class="err"> ψ ) → A t [ϕ t ↦ a t] )</span>
 </span><span id="__span-21-16"><a id="__codelineno-21-16" name="__codelineno-21-16" href="#__codelineno-21-16"></a><span class="err">      ( </span><span class="p">\ </span>g <span class="err">→ (f = g) )</span>
 </span><span id="__span-21-17"><a id="__codelineno-21-17" name="__codelineno-21-17" href="#__codelineno-21-17"></a><span class="err">      </span><span class="p">( </span>\ g → (t <span class="p">:</span><span class="err"> ψ ) → (f t = g t) [ϕ t ↦ </span><span class="s">refl</span><span class="err">])</span>
@@ -2175,7 +2175,7 @@ <h3 id="pointwise-homotopy-extension-types">Pointwise homotopy extension types<a
 </span><span id="__span-34-17"><a id="__codelineno-34-17" name="__codelineno-34-17" href="#__codelineno-34-17"></a><span class="err">    ( homotopy-extension-type I ψ ϕ A σ)</span>
 </span><span id="__span-34-18"><a id="__codelineno-34-18" name="__codelineno-34-18" href="#__codelineno-34-18"></a><span class="err">    ( pointwise-homotopy-extension-type σ)</span>
 </span><span id="__span-34-19"><a id="__codelineno-34-19" name="__codelineno-34-19" href="#__codelineno-34-19"></a><span class="err">  :=</span>
-</span><span id="__span-34-20"><a id="__codelineno-34-20" name="__codelineno-34-20" href="#__codelineno-34-20"></a><span class="err">    total-equiv-family-equiv</span>
+</span><span id="__span-34-20"><a id="__codelineno-34-20" name="__codelineno-34-20" href="#__codelineno-34-20"></a><span class="err">    total-equiv-family-of-equiv</span>
 </span><span id="__span-34-21"><a id="__codelineno-34-21" name="__codelineno-34-21" href="#__codelineno-34-21"></a><span class="err">    </span><span class="p">( </span>(t <span class="p">:</span><span class="err"> ψ) → A t)</span>
 </span><span id="__span-34-22"><a id="__codelineno-34-22" name="__codelineno-34-22" href="#__codelineno-34-22"></a><span class="err">    ( </span><span class="p">\ </span>τ <span class="err">→ (</span><span class="p">\ </span>t <span class="err">→ τ t) =_{ </span><span class="p">(</span>t <span class="p">:</span><span class="err"> ϕ) → A t} σ)</span>
 </span><span id="__span-34-23"><a id="__codelineno-34-23" name="__codelineno-34-23" href="#__codelineno-34-23"></a><span class="err">    </span><span class="p">( </span>\ τ → (t <span class="p">:</span><span class="err"> ϕ) → (τ t = σ t))</span>
@@ -2230,7 +2230,7 @@ <h2 id="relative-extension-types">Relative extension types<a class="headerlink"
 </span><span id="__span-35-28"><a id="__codelineno-35-28" name="__codelineno-35-28" href="#__codelineno-35-28"></a><span class="err">    ( relative-extension-type&#39;)</span>
 </span><span id="__span-35-29"><a id="__codelineno-35-29" name="__codelineno-35-29" href="#__codelineno-35-29"></a><span class="err">    ( relative-extension-type)</span>
 </span><span id="__span-35-30"><a id="__codelineno-35-30" name="__codelineno-35-30" href="#__codelineno-35-30"></a><span class="err">  :=</span>
-</span><span id="__span-35-31"><a id="__codelineno-35-31" name="__codelineno-35-31" href="#__codelineno-35-31"></a><span class="err">    total-equiv-family-equiv</span>
+</span><span id="__span-35-31"><a id="__codelineno-35-31" name="__codelineno-35-31" href="#__codelineno-35-31"></a><span class="err">    total-equiv-family-of-equiv</span>
 </span><span id="__span-35-32"><a id="__codelineno-35-32" name="__codelineno-35-32" href="#__codelineno-35-32"></a><span class="err">    </span><span class="p">( </span>(t <span class="p">:</span><span class="err"> ψ) → A&#39; t [ϕ t ↦ σ&#39; t])</span>
 </span><span id="__span-35-33"><a id="__codelineno-35-33" name="__codelineno-35-33" href="#__codelineno-35-33"></a><span class="err">    ( </span><span class="p">\ </span>τ&#39; <span class="err">→ (</span><span class="p">\ </span>t <span class="err">→ α t (τ&#39; t)) =_{ </span><span class="p">(</span>t <span class="p">:</span><span class="err"> ψ) → A t [ϕ t ↦ α t (σ&#39; t)]} τ)</span>
 </span><span id="__span-35-34"><a id="__codelineno-35-34" name="__codelineno-35-34" href="#__codelineno-35-34"></a><span class="err">    </span><span class="p">( </span>\ τ&#39; → (t <span class="p">:</span><span class="err"> ψ) → (α t (τ&#39; t) = τ t) [ϕ t ↦ </span><span class="s">refl</span><span class="err">])</span>

simplicial-hott/05-segal-types.rzk/index.html

@@ -2263,7 +2263,7 @@ <h2 id="homotopies">Homotopies<a class="headerlink" href="#homotopies" title="Pe
 </span><span id="__span-42-6"><a id="__codelineno-42-6" name="__codelineno-42-6" href="#__codelineno-42-6"></a><span class="err">  : Equiv (f = h) (hom2 A x x y (id-hom A x) f h)</span>
 </span><span id="__span-42-7"><a id="__codelineno-42-7" name="__codelineno-42-7" href="#__codelineno-42-7"></a><span class="err">  :=</span>
 </span><span id="__span-42-8"><a id="__codelineno-42-8" name="__codelineno-42-8" href="#__codelineno-42-8"></a><span class="err">    ( ( map-hom2-homotopy A x y f h) ,</span>
-</span><span id="__span-42-9"><a id="__codelineno-42-9" name="__codelineno-42-9" href="#__codelineno-42-9"></a><span class="err">      ( total-equiv-family-of-equiv</span>
+</span><span id="__span-42-9"><a id="__codelineno-42-9" name="__codelineno-42-9" href="#__codelineno-42-9"></a><span class="err">      ( is-equiv-fiberwise-is-equiv-total</span>
 </span><span id="__span-42-10"><a id="__codelineno-42-10" name="__codelineno-42-10" href="#__codelineno-42-10"></a><span class="err">        ( hom A x y)</span>
 </span><span id="__span-42-11"><a id="__codelineno-42-11" name="__codelineno-42-11" href="#__codelineno-42-11"></a><span class="err">        ( </span><span class="p">\ </span>k <span class="err">→ (f = k))</span>
 </span><span id="__span-42-12"><a id="__codelineno-42-12" name="__codelineno-42-12" href="#__codelineno-42-12"></a><span class="err">        ( </span><span class="p">\ </span>k <span class="err">→ (hom2 A x x y (id-hom A x) f k))</span>
@@ -2320,7 +2320,7 @@ <h2 id="homotopies">Homotopies<a class="headerlink" href="#homotopies" title="Pe
 </span><span id="__span-44-6"><a id="__codelineno-44-6" name="__codelineno-44-6" href="#__codelineno-44-6"></a><span class="err">  : Equiv (f = h) (hom2 A x y y f (id-hom A y) h)</span>
 </span><span id="__span-44-7"><a id="__codelineno-44-7" name="__codelineno-44-7" href="#__codelineno-44-7"></a><span class="err">  :=</span>
 </span><span id="__span-44-8"><a id="__codelineno-44-8" name="__codelineno-44-8" href="#__codelineno-44-8"></a><span class="err">    ( ( map-hom2-homotopy&#39; A x y f h) ,</span>
-</span><span id="__span-44-9"><a id="__codelineno-44-9" name="__codelineno-44-9" href="#__codelineno-44-9"></a><span class="err">      ( total-equiv-family-of-equiv</span>
+</span><span id="__span-44-9"><a id="__codelineno-44-9" name="__codelineno-44-9" href="#__codelineno-44-9"></a><span class="err">      ( is-equiv-fiberwise-is-equiv-total</span>
 </span><span id="__span-44-10"><a id="__codelineno-44-10" name="__codelineno-44-10" href="#__codelineno-44-10"></a><span class="err">        ( hom A x y)</span>
 </span><span id="__span-44-11"><a id="__codelineno-44-11" name="__codelineno-44-11" href="#__codelineno-44-11"></a><span class="err">        ( </span><span class="p">\ </span>k <span class="err">→ (f = k))</span>
 </span><span id="__span-44-12"><a id="__codelineno-44-12" name="__codelineno-44-12" href="#__codelineno-44-12"></a><span class="err">        ( </span><span class="p">\ </span>k <span class="err">→ (hom2 A x y y f (id-hom A y) k))</span>
@@ -2386,7 +2386,7 @@ <h2 id="homotopies">Homotopies<a class="headerlink" href="#homotopies" title="Pe
 </span><span id="__span-46-8"><a id="__codelineno-46-8" name="__codelineno-46-8" href="#__codelineno-46-8"></a><span class="err">  : Equiv ((comp-is-segal A is-segal-A x y z f g) = k) (hom2 A x y z f g k)</span>
 </span><span id="__span-46-9"><a id="__codelineno-46-9" name="__codelineno-46-9" href="#__codelineno-46-9"></a><span class="err">  :=</span>
 </span><span id="__span-46-10"><a id="__codelineno-46-10" name="__codelineno-46-10" href="#__codelineno-46-10"></a><span class="err">    ( ( map-hom2-eq-is-segal A is-segal-A x y z f g k) ,</span>
-</span><span id="__span-46-11"><a id="__codelineno-46-11" name="__codelineno-46-11" href="#__codelineno-46-11"></a><span class="err">      ( total-equiv-family-of-equiv</span>
+</span><span id="__span-46-11"><a id="__codelineno-46-11" name="__codelineno-46-11" href="#__codelineno-46-11"></a><span class="err">      ( is-equiv-fiberwise-is-equiv-total</span>
 </span><span id="__span-46-12"><a id="__codelineno-46-12" name="__codelineno-46-12" href="#__codelineno-46-12"></a><span class="err">        ( hom A x z)</span>
 </span><span id="__span-46-13"><a id="__codelineno-46-13" name="__codelineno-46-13" href="#__codelineno-46-13"></a><span class="err">        ( </span><span class="p">\ </span>m <span class="err">→ (comp-is-segal A is-segal-A x y z f g) = m)</span>
 </span><span id="__span-46-14"><a id="__codelineno-46-14" name="__codelineno-46-14" href="#__codelineno-46-14"></a><span class="err">        ( hom2 A x y z f g)</span>