-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cubical.Foundations.Equiv.Base.html
33 lines (26 loc) · 20.1 KB
/
Cubical.Foundations.Equiv.Base.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Cubical.Foundations.Equiv.Base</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Symbol">#-}</a>
<a id="24" class="Keyword">module</a> <a id="31" href="Cubical.Foundations.Equiv.Base.html" class="Module">Cubical.Foundations.Equiv.Base</a> <a id="62" class="Keyword">where</a>
<a id="69" class="Keyword">open</a> <a id="74" class="Keyword">import</a> <a id="81" href="Cubical.Foundations.Function.html" class="Module">Cubical.Foundations.Function</a>
<a id="110" class="Keyword">open</a> <a id="115" class="Keyword">import</a> <a id="122" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
<a id="151" class="Keyword">open</a> <a id="156" class="Keyword">import</a> <a id="163" href="Cubical.Core.Glue.html" class="Module">Cubical.Core.Glue</a> <a id="181" class="Keyword">public</a>
<a id="190" class="Keyword">using</a> <a id="196" class="Symbol">(</a> <a id="198" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="206" class="Symbol">;</a> <a id="208" href="Agda.Builtin.Cubical.Glue.html#971" class="Field">equiv-proof</a> <a id="220" class="Symbol">;</a> <a id="222" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">_≃_</a> <a id="226" class="Symbol">;</a> <a id="228" href="Agda.Builtin.Cubical.Glue.html#1143" class="Function">equivFun</a> <a id="237" class="Symbol">;</a> <a id="239" href="Agda.Builtin.Cubical.Glue.html#1455" class="Function">equivProof</a> <a id="250" class="Symbol">)</a>
<a id="fiber"></a><a id="253" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="259" class="Symbol">:</a> <a id="261" class="Symbol">∀</a> <a id="263" class="Symbol">{</a><a id="264" href="Cubical.Foundations.Equiv.Base.html#264" class="Bound">ℓ</a> <a id="266" href="Cubical.Foundations.Equiv.Base.html#266" class="Bound">ℓ'</a><a id="268" class="Symbol">}</a> <a id="270" class="Symbol">{</a><a id="271" href="Cubical.Foundations.Equiv.Base.html#271" class="Bound">A</a> <a id="273" class="Symbol">:</a> <a id="275" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="280" href="Cubical.Foundations.Equiv.Base.html#264" class="Bound">ℓ</a><a id="281" class="Symbol">}</a> <a id="283" class="Symbol">{</a><a id="284" href="Cubical.Foundations.Equiv.Base.html#284" class="Bound">B</a> <a id="286" class="Symbol">:</a> <a id="288" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="293" href="Cubical.Foundations.Equiv.Base.html#266" class="Bound">ℓ'</a><a id="295" class="Symbol">}</a> <a id="297" class="Symbol">(</a><a id="298" href="Cubical.Foundations.Equiv.Base.html#298" class="Bound">f</a> <a id="300" class="Symbol">:</a> <a id="302" href="Cubical.Foundations.Equiv.Base.html#271" class="Bound">A</a> <a id="304" class="Symbol">→</a> <a id="306" href="Cubical.Foundations.Equiv.Base.html#284" class="Bound">B</a><a id="307" class="Symbol">)</a> <a id="309" class="Symbol">(</a><a id="310" href="Cubical.Foundations.Equiv.Base.html#310" class="Bound">y</a> <a id="312" class="Symbol">:</a> <a id="314" href="Cubical.Foundations.Equiv.Base.html#284" class="Bound">B</a><a id="315" class="Symbol">)</a> <a id="317" class="Symbol">→</a> <a id="319" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="324" class="Symbol">(</a><a id="325" href="Agda.Primitive.html#810" class="Primitive">ℓ-max</a> <a id="331" href="Cubical.Foundations.Equiv.Base.html#264" class="Bound">ℓ</a> <a id="333" href="Cubical.Foundations.Equiv.Base.html#266" class="Bound">ℓ'</a><a id="335" class="Symbol">)</a>
<a id="337" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="343" class="Symbol">{</a><a id="344" class="Argument">A</a> <a id="346" class="Symbol">=</a> <a id="348" href="Cubical.Foundations.Equiv.Base.html#348" class="Bound">A</a><a id="349" class="Symbol">}</a> <a id="351" href="Cubical.Foundations.Equiv.Base.html#351" class="Bound">f</a> <a id="353" href="Cubical.Foundations.Equiv.Base.html#353" class="Bound">y</a> <a id="355" class="Symbol">=</a> <a id="357" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="360" href="Cubical.Foundations.Equiv.Base.html#360" class="Bound">x</a> <a id="362" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="364" href="Cubical.Foundations.Equiv.Base.html#348" class="Bound">A</a> <a id="366" href="Cubical.Core.Primitives.html#6306" class="Function">]</a> <a id="368" href="Cubical.Foundations.Equiv.Base.html#351" class="Bound">f</a> <a id="370" href="Cubical.Foundations.Equiv.Base.html#360" class="Bound">x</a> <a id="372" href="Agda.Builtin.Cubical.Path.html#388" class="Function Operator">≡</a> <a id="374" href="Cubical.Foundations.Equiv.Base.html#353" class="Bound">y</a>
<a id="377" class="Comment">-- Helper function for constructing equivalences from pairs (f,g) that cancel each other up to definitional</a>
<a id="485" class="Comment">-- equality. For such (f,g), the result type simplifies to isContr (fiber f b).</a>
<a id="strictContrFibers"></a><a id="565" href="Cubical.Foundations.Equiv.Base.html#565" class="Function">strictContrFibers</a> <a id="583" class="Symbol">:</a> <a id="585" class="Symbol">∀</a> <a id="587" class="Symbol">{</a><a id="588" href="Cubical.Foundations.Equiv.Base.html#588" class="Bound">ℓ</a> <a id="590" href="Cubical.Foundations.Equiv.Base.html#590" class="Bound">ℓ'</a><a id="592" class="Symbol">}</a> <a id="594" class="Symbol">{</a><a id="595" href="Cubical.Foundations.Equiv.Base.html#595" class="Bound">A</a> <a id="597" class="Symbol">:</a> <a id="599" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="604" href="Cubical.Foundations.Equiv.Base.html#588" class="Bound">ℓ</a><a id="605" class="Symbol">}</a> <a id="607" class="Symbol">{</a><a id="608" href="Cubical.Foundations.Equiv.Base.html#608" class="Bound">B</a> <a id="610" class="Symbol">:</a> <a id="612" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="617" href="Cubical.Foundations.Equiv.Base.html#590" class="Bound">ℓ'</a><a id="619" class="Symbol">}</a> <a id="621" class="Symbol">{</a><a id="622" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="624" class="Symbol">:</a> <a id="626" href="Cubical.Foundations.Equiv.Base.html#595" class="Bound">A</a> <a id="628" class="Symbol">→</a> <a id="630" href="Cubical.Foundations.Equiv.Base.html#608" class="Bound">B</a><a id="631" class="Symbol">}</a> <a id="633" class="Symbol">(</a><a id="634" href="Cubical.Foundations.Equiv.Base.html#634" class="Bound">g</a> <a id="636" class="Symbol">:</a> <a id="638" href="Cubical.Foundations.Equiv.Base.html#608" class="Bound">B</a> <a id="640" class="Symbol">→</a> <a id="642" href="Cubical.Foundations.Equiv.Base.html#595" class="Bound">A</a><a id="643" class="Symbol">)</a> <a id="645" class="Symbol">(</a><a id="646" href="Cubical.Foundations.Equiv.Base.html#646" class="Bound">b</a> <a id="648" class="Symbol">:</a> <a id="650" href="Cubical.Foundations.Equiv.Base.html#608" class="Bound">B</a><a id="651" class="Symbol">)</a>
<a id="655" class="Symbol">→</a> <a id="657" href="Cubical.Core.Primitives.html#6306" class="Function">Σ[</a> <a id="660" href="Cubical.Foundations.Equiv.Base.html#660" class="Bound">t</a> <a id="662" href="Cubical.Core.Primitives.html#6306" class="Function">∈</a> <a id="664" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="670" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="672" class="Symbol">(</a><a id="673" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="675" class="Symbol">(</a><a id="676" href="Cubical.Foundations.Equiv.Base.html#634" class="Bound">g</a> <a id="678" href="Cubical.Foundations.Equiv.Base.html#646" class="Bound">b</a><a id="679" class="Symbol">))</a> <a id="682" href="Cubical.Core.Primitives.html#6306" class="Function">]</a>
<a id="688" class="Symbol">((</a><a id="690" href="Cubical.Foundations.Equiv.Base.html#690" class="Bound">t'</a> <a id="693" class="Symbol">:</a> <a id="695" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="701" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="703" href="Cubical.Foundations.Equiv.Base.html#646" class="Bound">b</a><a id="704" class="Symbol">)</a> <a id="706" class="Symbol">→</a> <a id="708" href="Cubical.Core.Primitives.html#1866" class="Function">Path</a> <a id="713" class="Symbol">(</a><a id="714" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="720" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="722" class="Symbol">(</a><a id="723" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="725" class="Symbol">(</a><a id="726" href="Cubical.Foundations.Equiv.Base.html#634" class="Bound">g</a> <a id="728" href="Cubical.Foundations.Equiv.Base.html#646" class="Bound">b</a><a id="729" class="Symbol">)))</a> <a id="733" href="Cubical.Foundations.Equiv.Base.html#660" class="Bound">t</a> <a id="735" class="Symbol">(</a><a id="736" href="Cubical.Foundations.Equiv.Base.html#634" class="Bound">g</a> <a id="738" class="Symbol">(</a><a id="739" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="741" class="Symbol">(</a><a id="742" href="Cubical.Foundations.Equiv.Base.html#690" class="Bound">t'</a> <a id="745" class="Symbol">.</a><a id="746" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a><a id="749" class="Symbol">))</a> <a id="752" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="754" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="759" class="Symbol">(</a><a id="760" href="Cubical.Foundations.Equiv.Base.html#622" class="Bound">f</a> <a id="762" href="Cubical.Foundations.Function.html#526" class="Function Operator">∘</a> <a id="764" href="Cubical.Foundations.Equiv.Base.html#634" class="Bound">g</a><a id="765" class="Symbol">)</a> <a id="767" class="Symbol">(</a><a id="768" href="Cubical.Foundations.Equiv.Base.html#690" class="Bound">t'</a> <a id="771" class="Symbol">.</a><a id="772" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a><a id="775" class="Symbol">)))</a>
<a id="779" href="Cubical.Foundations.Equiv.Base.html#565" class="Function">strictContrFibers</a> <a id="797" class="Symbol">{</a><a id="798" class="Argument">f</a> <a id="800" class="Symbol">=</a> <a id="802" href="Cubical.Foundations.Equiv.Base.html#802" class="Bound">f</a><a id="803" class="Symbol">}</a> <a id="805" href="Cubical.Foundations.Equiv.Base.html#805" class="Bound">g</a> <a id="807" href="Cubical.Foundations.Equiv.Base.html#807" class="Bound">b</a> <a id="809" class="Symbol">.</a><a id="810" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="814" class="Symbol">=</a> <a id="816" class="Symbol">(</a><a id="817" href="Cubical.Foundations.Equiv.Base.html#805" class="Bound">g</a> <a id="819" href="Cubical.Foundations.Equiv.Base.html#807" class="Bound">b</a> <a id="821" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="823" href="Cubical.Foundations.Prelude.html#915" class="Function">refl</a><a id="827" class="Symbol">)</a>
<a id="829" href="Cubical.Foundations.Equiv.Base.html#565" class="Function">strictContrFibers</a> <a id="847" class="Symbol">{</a><a id="848" class="Argument">f</a> <a id="850" class="Symbol">=</a> <a id="852" href="Cubical.Foundations.Equiv.Base.html#852" class="Bound">f</a><a id="853" class="Symbol">}</a> <a id="855" href="Cubical.Foundations.Equiv.Base.html#855" class="Bound">g</a> <a id="857" href="Cubical.Foundations.Equiv.Base.html#857" class="Bound">b</a> <a id="859" class="Symbol">.</a><a id="860" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="864" class="Symbol">(</a><a id="865" href="Cubical.Foundations.Equiv.Base.html#865" class="Bound">a</a> <a id="867" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="869" href="Cubical.Foundations.Equiv.Base.html#869" class="Bound">p</a><a id="870" class="Symbol">)</a> <a id="872" href="Cubical.Foundations.Equiv.Base.html#872" class="Bound">i</a> <a id="874" class="Symbol">=</a> <a id="876" class="Symbol">(</a><a id="877" href="Cubical.Foundations.Equiv.Base.html#855" class="Bound">g</a> <a id="879" class="Symbol">(</a><a id="880" href="Cubical.Foundations.Equiv.Base.html#869" class="Bound">p</a> <a id="882" class="Symbol">(</a><a id="883" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="885" href="Cubical.Foundations.Equiv.Base.html#872" class="Bound">i</a><a id="886" class="Symbol">))</a> <a id="889" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="891" class="Symbol">λ</a> <a id="893" href="Cubical.Foundations.Equiv.Base.html#893" class="Bound">j</a> <a id="895" class="Symbol">→</a> <a id="897" href="Cubical.Foundations.Equiv.Base.html#852" class="Bound">f</a> <a id="899" class="Symbol">(</a><a id="900" href="Cubical.Foundations.Equiv.Base.html#855" class="Bound">g</a> <a id="902" class="Symbol">(</a><a id="903" href="Cubical.Foundations.Equiv.Base.html#869" class="Bound">p</a> <a id="905" class="Symbol">(</a><a id="906" href="Cubical.Core.Primitives.html#539" class="Primitive Operator">~</a> <a id="908" href="Cubical.Foundations.Equiv.Base.html#872" class="Bound">i</a> <a id="910" href="Cubical.Core.Primitives.html#490" class="Primitive Operator">∨</a> <a id="912" href="Cubical.Foundations.Equiv.Base.html#893" class="Bound">j</a><a id="913" class="Symbol">))))</a>
<a id="919" class="Comment">-- The identity equivalence</a>
<a id="idIsEquiv"></a><a id="947" href="Cubical.Foundations.Equiv.Base.html#947" class="Function">idIsEquiv</a> <a id="957" class="Symbol">:</a> <a id="959" class="Symbol">∀</a> <a id="961" class="Symbol">{</a><a id="962" href="Cubical.Foundations.Equiv.Base.html#962" class="Bound">ℓ</a><a id="963" class="Symbol">}</a> <a id="965" class="Symbol">(</a><a id="966" href="Cubical.Foundations.Equiv.Base.html#966" class="Bound">A</a> <a id="968" class="Symbol">:</a> <a id="970" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="975" href="Cubical.Foundations.Equiv.Base.html#962" class="Bound">ℓ</a><a id="976" class="Symbol">)</a> <a id="978" class="Symbol">→</a> <a id="980" href="Agda.Builtin.Cubical.Glue.html#868" class="Record">isEquiv</a> <a id="988" class="Symbol">(</a><a id="989" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="995" href="Cubical.Foundations.Equiv.Base.html#966" class="Bound">A</a><a id="996" class="Symbol">)</a>
<a id="998" href="Cubical.Foundations.Equiv.Base.html#947" class="Function">idIsEquiv</a> <a id="1008" href="Cubical.Foundations.Equiv.Base.html#1008" class="Bound">A</a> <a id="1010" class="Symbol">.</a><a id="1011" href="Agda.Builtin.Cubical.Glue.html#971" class="Field">equiv-proof</a> <a id="1023" class="Symbol">=</a> <a id="1025" href="Cubical.Foundations.Equiv.Base.html#565" class="Function">strictContrFibers</a> <a id="1043" class="Symbol">(</a><a id="1044" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="1050" href="Cubical.Foundations.Equiv.Base.html#1008" class="Bound">A</a><a id="1051" class="Symbol">)</a>
<a id="idEquiv"></a><a id="1054" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1062" class="Symbol">:</a> <a id="1064" class="Symbol">∀</a> <a id="1066" class="Symbol">{</a><a id="1067" href="Cubical.Foundations.Equiv.Base.html#1067" class="Bound">ℓ</a><a id="1068" class="Symbol">}</a> <a id="1070" class="Symbol">(</a><a id="1071" href="Cubical.Foundations.Equiv.Base.html#1071" class="Bound">A</a> <a id="1073" class="Symbol">:</a> <a id="1075" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1080" href="Cubical.Foundations.Equiv.Base.html#1067" class="Bound">ℓ</a><a id="1081" class="Symbol">)</a> <a id="1083" class="Symbol">→</a> <a id="1085" href="Cubical.Foundations.Equiv.Base.html#1071" class="Bound">A</a> <a id="1087" href="Agda.Builtin.Cubical.Glue.html#1051" class="Function Operator">≃</a> <a id="1089" href="Cubical.Foundations.Equiv.Base.html#1071" class="Bound">A</a>
<a id="1091" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1099" href="Cubical.Foundations.Equiv.Base.html#1099" class="Bound">A</a> <a id="1101" class="Symbol">.</a><a id="1102" href="Agda.Builtin.Sigma.html#252" class="Field">fst</a> <a id="1106" class="Symbol">=</a> <a id="1108" href="Cubical.Foundations.Function.html#468" class="Function">idfun</a> <a id="1114" href="Cubical.Foundations.Equiv.Base.html#1099" class="Bound">A</a>
<a id="1116" href="Cubical.Foundations.Equiv.Base.html#1054" class="Function">idEquiv</a> <a id="1124" href="Cubical.Foundations.Equiv.Base.html#1124" class="Bound">A</a> <a id="1126" class="Symbol">.</a><a id="1127" href="Agda.Builtin.Sigma.html#264" class="Field">snd</a> <a id="1131" class="Symbol">=</a> <a id="1133" href="Cubical.Foundations.Equiv.Base.html#947" class="Function">idIsEquiv</a> <a id="1143" href="Cubical.Foundations.Equiv.Base.html#1124" class="Bound">A</a>
<a id="1146" class="Comment">-- the definition using Π-type</a>
<a id="isEquiv'"></a><a id="1177" href="Cubical.Foundations.Equiv.Base.html#1177" class="Function">isEquiv'</a> <a id="1186" class="Symbol">:</a> <a id="1188" class="Symbol">∀</a> <a id="1190" class="Symbol">{</a><a id="1191" href="Cubical.Foundations.Equiv.Base.html#1191" class="Bound">ℓ</a><a id="1192" class="Symbol">}{</a><a id="1194" href="Cubical.Foundations.Equiv.Base.html#1194" class="Bound">ℓ'</a><a id="1196" class="Symbol">}{</a><a id="1198" href="Cubical.Foundations.Equiv.Base.html#1198" class="Bound">A</a> <a id="1200" class="Symbol">:</a> <a id="1202" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1207" href="Cubical.Foundations.Equiv.Base.html#1191" class="Bound">ℓ</a><a id="1208" class="Symbol">}{</a><a id="1210" href="Cubical.Foundations.Equiv.Base.html#1210" class="Bound">B</a> <a id="1212" class="Symbol">:</a> <a id="1214" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1219" href="Cubical.Foundations.Equiv.Base.html#1194" class="Bound">ℓ'</a><a id="1221" class="Symbol">}</a> <a id="1223" class="Symbol">→</a> <a id="1225" class="Symbol">(</a><a id="1226" href="Cubical.Foundations.Equiv.Base.html#1198" class="Bound">A</a> <a id="1228" class="Symbol">→</a> <a id="1230" href="Cubical.Foundations.Equiv.Base.html#1210" class="Bound">B</a><a id="1231" class="Symbol">)</a> <a id="1233" class="Symbol">→</a> <a id="1235" href="Agda.Primitive.html#326" class="Primitive">Type</a> <a id="1240" class="Symbol">(</a><a id="1241" href="Agda.Primitive.html#810" class="Primitive">ℓ-max</a> <a id="1247" href="Cubical.Foundations.Equiv.Base.html#1191" class="Bound">ℓ</a> <a id="1249" href="Cubical.Foundations.Equiv.Base.html#1194" class="Bound">ℓ'</a><a id="1251" class="Symbol">)</a>
<a id="1253" href="Cubical.Foundations.Equiv.Base.html#1177" class="Function">isEquiv'</a> <a id="1262" class="Symbol">{</a><a id="1263" class="Argument">B</a> <a id="1265" class="Symbol">=</a> <a id="1267" href="Cubical.Foundations.Equiv.Base.html#1267" class="Bound">B</a><a id="1268" class="Symbol">}</a> <a id="1270" href="Cubical.Foundations.Equiv.Base.html#1270" class="Bound">f</a> <a id="1272" class="Symbol">=</a> <a id="1274" class="Symbol">(</a><a id="1275" href="Cubical.Foundations.Equiv.Base.html#1275" class="Bound">y</a> <a id="1277" class="Symbol">:</a> <a id="1279" href="Cubical.Foundations.Equiv.Base.html#1267" class="Bound">B</a><a id="1280" class="Symbol">)</a> <a id="1282" class="Symbol">→</a> <a id="1284" href="Cubical.Foundations.Prelude.html#13975" class="Function">isContr</a> <a id="1292" class="Symbol">(</a><a id="1293" href="Cubical.Foundations.Equiv.Base.html#253" class="Function">fiber</a> <a id="1299" href="Cubical.Foundations.Equiv.Base.html#1270" class="Bound">f</a> <a id="1301" href="Cubical.Foundations.Equiv.Base.html#1275" class="Bound">y</a><a id="1302" class="Symbol">)</a>
</pre></body></html>