Skip to content

Commit

Permalink
Deploying to gh-pages from @ 5427228 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Oct 2, 2023
1 parent 2330a9d commit 7871e34
Show file tree
Hide file tree
Showing 83 changed files with 3,665 additions and 3,590 deletions.
48 changes: 24 additions & 24 deletions Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod.html
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
<a id="537" class="Keyword">variable</a>
<a id="550" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#550" class="Generalizable">ℓ</a> <a id="552" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#552" class="Generalizable">ℓ&#39;</a> <a id="555" class="Symbol">:</a> <a id="557" href="Agda.Primitive.html#591" class="Postulate">Level</a>

<a id="564" class="Keyword">module</a> <a id="571" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#571" class="Module">_</a> <a id="573" class="Symbol">{</a><a id="574" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#574" class="Bound">A</a> <a id="576" class="Symbol">:</a> <a id="578" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="583" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#550" class="Generalizable">ℓ</a><a id="584" class="Symbol">}</a> <a id="586" class="Symbol">(</a><a id="587" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#587" class="Bound">conA</a> <a id="592" class="Symbol">:</a> <a id="594" href="Cubical.Homotopy.Connected.html#1273" class="Function">isConnected</a> <a id="606" class="Number">2</a> <a id="608" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#574" class="Bound">A</a><a id="609" class="Symbol">)</a> <a id="611" class="Symbol">(</a><a id="612" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#612" class="Bound">G</a> <a id="614" class="Symbol">:</a> <a id="616" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="624" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#552" class="Generalizable">ℓ&#39;</a><a id="626" class="Symbol">)</a> <a id="628" class="Keyword">where</a>
<a id="564" class="Keyword">module</a> <a id="571" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#571" class="Module">_</a> <a id="573" class="Symbol">{</a><a id="574" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#574" class="Bound">A</a> <a id="576" class="Symbol">:</a> <a id="578" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="583" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#550" class="Generalizable">ℓ</a><a id="584" class="Symbol">}</a> <a id="586" class="Symbol">(</a><a id="587" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#587" class="Bound">conA</a> <a id="592" class="Symbol">:</a> <a id="594" href="Cubical.Homotopy.Connected.html#1432" class="Function">isConnected</a> <a id="606" class="Number">2</a> <a id="608" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#574" class="Bound">A</a><a id="609" class="Symbol">)</a> <a id="611" class="Symbol">(</a><a id="612" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#612" class="Bound">G</a> <a id="614" class="Symbol">:</a> <a id="616" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="624" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#552" class="Generalizable">ℓ&#39;</a><a id="626" class="Symbol">)</a> <a id="628" class="Keyword">where</a>
<a id="636" class="Keyword">private</a>
<a id="648" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#648" class="Function">H⁰A</a> <a id="652" class="Symbol">=</a> <a id="654" href="Cubical.Cohomology.EilenbergMacLane.Base.html#1308" class="Function">coHom</a> <a id="660" class="Number">0</a> <a id="662" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#612" class="Bound">G</a> <a id="664" href="Cubical.Cohomology.EilenbergMacLane.Groups.Connected.html#574" class="Bound">A</a>

Expand Down
38 changes: 19 additions & 19 deletions Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle.html
View file

Large diffs are not rendered by default.

26 changes: 13 additions & 13 deletions Cubical.Cohomology.EilenbergMacLane.Groups.RP2.html
View file

Large diffs are not rendered by default.

78 changes: 39 additions & 39 deletions Cubical.Cohomology.EilenbergMacLane.Groups.Sn.html
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,13 +74,13 @@
<a id="2289" class="Symbol">(λ</a> <a id="2292" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2292" class="Bound">p</a> <a id="2294" class="Symbol">→</a> <a id="2296" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2301" href="Cubical.HITs.SetTruncation.Base.html#299" class="InductiveConstructor Operator">∣_∣₂</a> <a id="2306" class="Symbol">(</a><a id="2307" href="Cubical.Foundations.Prelude.html#9927" class="Function">funExt</a> <a id="2314" class="Symbol">λ</a> <a id="2316" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2316" class="Bound">x</a> <a id="2318" class="Symbol">→</a> <a id="2320" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2325" class="Symbol">(λ</a> <a id="2328" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2328" class="Bound">z</a> <a id="2330" class="Symbol">→</a> <a id="2332" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2204" class="Bound">f</a> <a id="2334" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2316" class="Bound">x</a> <a id="2336" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3350" class="Function">+[</a> <a id="2339" class="Symbol">(</a><a id="2340" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2344" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2345" class="Symbol">)</a> <a id="2347" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3350" class="Function">]ₖ</a> <a id="2350" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2328" class="Bound">z</a><a id="2351" class="Symbol">)</a>
<a id="2386" class="Symbol">(</a><a id="2387" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2392" class="Symbol">(λ</a> <a id="2395" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2395" class="Bound">z</a> <a id="2397" class="Symbol">→</a> <a id="2399" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3430" class="Function">-[</a> <a id="2402" class="Symbol">(</a><a id="2403" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2407" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2408" class="Symbol">)</a> <a id="2410" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3430" class="Function">]ₖ</a> <a id="2413" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2395" class="Bound">z</a><a id="2414" class="Symbol">)</a> <a id="2416" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2292" class="Bound">p</a> <a id="2418" href="Cubical.Foundations.Prelude.html#4446" class="Function Operator">∙</a> <a id="2420" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#15981" class="Function">-0ₖ</a> <a id="2424" class="Symbol">(</a><a id="2425" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2429" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2430" class="Symbol">))</a>
<a id="2463" href="Cubical.Foundations.Prelude.html#4446" class="Function Operator">∙</a> <a id="2465" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3896" class="Function">rUnitₖ</a> <a id="2472" class="Symbol">(</a><a id="2473" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2477" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2478" class="Symbol">)</a> <a id="2480" class="Symbol">(</a><a id="2481" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2204" class="Bound">f</a> <a id="2483" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2316" class="Bound">x</a><a id="2484" class="Symbol">)))</a>
<a id="2502" class="Symbol">(</a><a id="2503" href="Cubical.Homotopy.Connected.html#12130" class="Function">isConnectedPath</a> <a id="2519" class="Symbol">(</a><a id="2520" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2524" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2525" class="Symbol">)</a>
<a id="2502" class="Symbol">(</a><a id="2503" href="Cubical.Homotopy.Connected.html#13165" class="Function">isConnectedPath</a> <a id="2519" class="Symbol">(</a><a id="2520" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2524" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2525" class="Symbol">)</a>
<a id="2542" class="Symbol">(</a><a id="2543" href="Cubical.Homotopy.EilenbergMacLane.Properties.html#1864" class="Function">isConnectedEM</a> <a id="2557" class="Symbol">(</a><a id="2558" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2562" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2563" class="Symbol">))</a> <a id="2566" class="Symbol">(</a><a id="2567" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2204" class="Bound">f</a> <a id="2569" class="Symbol">(</a><a id="2570" href="Cubical.Foundations.Pointed.Base.html#540" class="Function">pt</a> <a id="2573" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#1005" class="Bound">A</a><a id="2574" class="Symbol">))</a> <a id="2577" class="Symbol">(</a><a id="2578" href="Cubical.Homotopy.EilenbergMacLane.Base.html#2488" class="Function">0ₖ</a> <a id="2581" class="Symbol">(</a><a id="2582" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2586" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2587" class="Symbol">))</a> <a id="2590" class="Symbol">.</a><a id="2591" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a><a id="2594" class="Symbol">)</a>
<a id="2608" href="Agda.Builtin.Sigma.html#218" class="InductiveConstructor Operator">,</a> <a id="2610" href="Cubical.HITs.Truncation.Properties.html#4831" class="Function">Trunc.rec</a> <a id="2620" class="Symbol">(</a><a id="2621" href="Cubical.Foundations.HLevels.html#2952" class="Function">isProp→isOfHLevelSuc</a> <a id="2642" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a> <a id="2644" class="Symbol">(</a><a id="2645" href="Cubical.HITs.SetTruncation.Base.html#319" class="InductiveConstructor">squash₂</a> <a id="2653" class="Symbol">_</a> <a id="2655" class="Symbol">_))</a>
<a id="2675" class="Symbol">(λ</a> <a id="2678" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2678" class="Bound">p</a> <a id="2680" class="Symbol">→</a> <a id="2682" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2687" href="Cubical.HITs.SetTruncation.Base.html#299" class="InductiveConstructor Operator">∣_∣₂</a> <a id="2692" class="Symbol">(</a><a id="2693" href="Cubical.Foundations.Prelude.html#9927" class="Function">funExt</a> <a id="2700" class="Symbol">λ</a> <a id="2702" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2702" class="Bound">x</a> <a id="2704" class="Symbol">→</a> <a id="2706" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2711" class="Symbol">(λ</a> <a id="2714" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2714" class="Bound">z</a> <a id="2716" class="Symbol">→</a> <a id="2718" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2206" class="Bound">g</a> <a id="2720" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2702" class="Bound">x</a> <a id="2722" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3350" class="Function">+[</a> <a id="2725" class="Symbol">(</a><a id="2726" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2730" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2731" class="Symbol">)</a> <a id="2733" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3350" class="Function">]ₖ</a> <a id="2736" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2714" class="Bound">z</a><a id="2737" class="Symbol">)</a>
<a id="2772" class="Symbol">(</a><a id="2773" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="2778" class="Symbol">(λ</a> <a id="2781" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2781" class="Bound">z</a> <a id="2783" class="Symbol">→</a> <a id="2785" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3430" class="Function">-[</a> <a id="2788" class="Symbol">(</a><a id="2789" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2793" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2794" class="Symbol">)</a> <a id="2796" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3430" class="Function">]ₖ</a> <a id="2799" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2781" class="Bound">z</a><a id="2800" class="Symbol">)</a> <a id="2802" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2678" class="Bound">p</a> <a id="2804" href="Cubical.Foundations.Prelude.html#4446" class="Function Operator">∙</a> <a id="2806" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#15981" class="Function">-0ₖ</a> <a id="2810" class="Symbol">(</a><a id="2811" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2815" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2816" class="Symbol">))</a>
<a id="2849" href="Cubical.Foundations.Prelude.html#4446" class="Function Operator">∙</a> <a id="2851" href="Cubical.Homotopy.EilenbergMacLane.GroupStructure.html#3896" class="Function">rUnitₖ</a> <a id="2858" class="Symbol">(</a><a id="2859" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2863" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2864" class="Symbol">)</a> <a id="2866" class="Symbol">(</a><a id="2867" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2206" class="Bound">g</a> <a id="2869" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2702" class="Bound">x</a><a id="2870" class="Symbol">)))</a>
<a id="2888" class="Symbol">(</a><a id="2889" href="Cubical.Homotopy.Connected.html#12130" class="Function">isConnectedPath</a> <a id="2905" class="Symbol">(</a><a id="2906" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2910" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2911" class="Symbol">)</a>
<a id="2888" class="Symbol">(</a><a id="2889" href="Cubical.Homotopy.Connected.html#13165" class="Function">isConnectedPath</a> <a id="2905" class="Symbol">(</a><a id="2906" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2910" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2911" class="Symbol">)</a>
<a id="2928" class="Symbol">(</a><a id="2929" href="Cubical.Homotopy.EilenbergMacLane.Properties.html#1864" class="Function">isConnectedEM</a> <a id="2943" class="Symbol">(</a><a id="2944" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2948" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2949" class="Symbol">))</a> <a id="2952" class="Symbol">(</a><a id="2953" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2206" class="Bound">g</a> <a id="2955" class="Symbol">(</a><a id="2956" href="Cubical.Foundations.Pointed.Base.html#540" class="Function">pt</a> <a id="2959" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#1021" class="Bound">B</a><a id="2960" class="Symbol">))</a> <a id="2963" class="Symbol">(</a><a id="2964" href="Cubical.Homotopy.EilenbergMacLane.Base.html#2488" class="Function">0ₖ</a> <a id="2967" class="Symbol">(</a><a id="2968" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="2972" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#2107" class="Bound">n</a><a id="2973" class="Symbol">))</a> <a id="2976" class="Symbol">.</a><a id="2977" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a><a id="2980" class="Symbol">)))</a>
<a id="2986" href="Cubical.Foundations.Isomorphism.html#948" class="Field">Iso.leftInv</a> <a id="2998" class="Symbol">(</a><a id="2999" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#1774" class="Function">Hⁿ⋁-Iso</a> <a id="3007" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#3007" class="Bound">n</a><a id="3008" class="Symbol">)</a> <a id="3010" class="Symbol">=</a>
<a id="3016" href="Cubical.HITs.SetTruncation.Properties.html#1425" class="Function">ST.elim</a> <a id="3024" class="Symbol">(λ</a> <a id="3027" href="Cubical.Cohomology.EilenbergMacLane.Groups.Wedge.html#3027" class="Bound">_</a> <a id="3029" class="Symbol">→</a> <a id="3031" href="Cubical.HITs.SetTruncation.Properties.html#738" class="Function">isSetPathImplicit</a><a id="3048" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit 7871e34

Please sign in to comment.