Skip to content

Commit

Permalink
Deploying to gh-pages from @ 63a47b4 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
jdchristensen committed Sep 26, 2024
0 parents commit 0b3bbfd
Show file tree
Hide file tree
Showing 2,698 changed files with 1,755,408 additions and 0 deletions.
389 changes: 389 additions & 0 deletions alectryon-html/HoTT.Algebra.AbGroups.AbHom.html

Large diffs are not rendered by default.

96 changes: 96 additions & 0 deletions alectryon-html/HoTT.Algebra.AbGroups.AbProjective.html

Large diffs are not rendered by default.

64 changes: 64 additions & 0 deletions alectryon-html/HoTT.Algebra.AbGroups.AbPullback.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
<title>AbPullback.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
<link rel="stylesheet" href="pygments.css" type="text/css" />
<script type="text/javascript" src="alectryon.js"></script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
<meta name="viewport" content="width=device-width, initial-scale=1">
</head>
<body>
<div class="alectryon-root alectryon-centered"><div class="alectryon-banner">Built with <a href="https://github.com/cpitclaudel/alectryon/">Alectryon</a>, running Coq+SerAPI v8.19.0+0.19.3. Bubbles (<span class="alectryon-bubble"></span>) indicate interactive fragments: hover for details, tap to reveal contents. Use <kbd>Ctrl+↑</kbd> <kbd>Ctrl+↓</kbd> to navigate, <kbd>Ctrl+🖱️</kbd> to focus. On Mac, use <kbd></kbd> instead of <kbd>Ctrl</kbd>.</div><div class="document">


<pre class="alectryon-io highlight"><!-- Generator: Alectryon --><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk0" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk0"><span class="kn">Require Import</span> Basics.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">[Loading ML file number_string_notation_plugin.cmxs (<span class="nb">using</span> legacy method) ... <span class="bp">done</span>]</blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Import</span> Limits.Pullback Cubical.PathSquare.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Export</span> Algebra.Groups.GrpPullback.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Import</span> Algebra.AbGroups.AbelianGroup.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Import</span> WildCat.Core.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp">
<span class="sd">(** * Pullbacks of abelian groups *)</span>

</span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Section</span> <span class="nf">AbPullback</span>.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> <span class="c">(* Variables are named to correspond with Limits.Pullback. *)</span>
</span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Context</span> {<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span> : AbGroup} (<span class="nv">f</span> : B $-&gt; A) (<span class="nv">g</span> : C $-&gt; A).</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp">
</span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk1" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk1"><span class="kn">Global Instance</span> <span class="nf">ab_pullback_commutative</span>
: Commutative (@group_sgop (grp_pullback f g)).</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">Commutative group_sgop</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk2" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk2"><span class="kn">Proof</span>.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">Commutative group_sgop</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk3" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk3"><span class="nb">unfold</span> Commutative.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">y</span> : grp_pullback f g,
group_sgop x y = group_sgop y x</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk4" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk4"><span class="nb">intros</span> [b [c p]] [d [e q]].</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br><span><var>b</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>c</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>p</var><span class="hyp-type"><b>: </b><span>f b = g c</span></span></span><br><span><var>d</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>e</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>q</var><span class="hyp-type"><b>: </b><span>f d = g e</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">group_sgop (b; c; p) (d; e; q) =
group_sgop (d; e; q) (b; c; p)</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk5" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk5"><span class="nb">apply</span> equiv_path_pullback; <span class="nb">simpl</span>.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br><span><var>b</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>c</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>p</var><span class="hyp-type"><b>: </b><span>f b = g c</span></span></span><br><span><var>d</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>e</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>q</var><span class="hyp-type"><b>: </b><span>f d = g e</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">{p0 : sg_op b d = sg_op d b &amp;
{q0 : sg_op c e = sg_op e c &amp;
PathSquare (ap f p0) (ap g q0)
(grp_homo_op_agree f g p q)
(grp_homo_op_agree f g q p)}}</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk6" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk6"><span class="nb">refine</span> (commutativity _ _; commutativity _ _; _).</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br><span><var>b</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>c</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>p</var><span class="hyp-type"><b>: </b><span>f b = g c</span></span></span><br><span><var>d</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>e</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>q</var><span class="hyp-type"><b>: </b><span>f d = g e</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">PathSquare (ap f (commutativity b d))
(ap g (commutativity c e))
(grp_homo_op_agree f g p q)
(grp_homo_op_agree f g q p)</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><input class="alectryon-toggle" id="abpullback-v-chk7" style="display: none" type="checkbox"><label class="alectryon-input" for="abpullback-v-chk7"><span class="nb">apply</span> equiv_sq_path.</label><small class="alectryon-output"><div><div class="alectryon-goals"><blockquote class="alectryon-goal"><div class="goal-hyps"><span><var>A, B, C</var><span class="hyp-type"><b>: </b><span>AbGroup</span></span></span><br><span><var>f</var><span class="hyp-type"><b>: </b><span>B $-&gt; A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-&gt; A</span></span></span><br><span><var>b</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>c</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>p</var><span class="hyp-type"><b>: </b><span>f b = g c</span></span></span><br><span><var>d</var><span class="hyp-type"><b>: </b><span>B</span></span></span><br><span><var>e</var><span class="hyp-type"><b>: </b><span>C</span></span></span><br><span><var>q</var><span class="hyp-type"><b>: </b><span>f d = g e</span></span></span><br></div><span class="goal-separator"><hr></span><div class="goal-conclusion">ap f (commutativity b d) @ grp_homo_op_agree f g q p =
grp_homo_op_agree f g p q @ ap g (commutativity c e)</div></blockquote></div></div></small><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="nb">apply</span> path_ishprop.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Defined</span>.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp">
</span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Global Instance</span> <span class="nf">isabgroup_ab_pullback</span>
: IsAbGroup (grp_pullback f g) := {}.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp">
</span><span class="alectryon-wsp"> </span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Definition</span> <span class="nf">ab_pullback</span>
: AbGroup := Build_AbGroup (grp_pullback f g) _.</span><span class="alectryon-wsp">
</span></span><span class="alectryon-wsp">
<span class="sd">(** The corecursion principle is inherited from Groups; use grp_pullback_corec and friends from Groups/GrpPullback.v. *)</span>

</span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">End</span> <span class="nf">AbPullback</span>.</span></span></pre>
</div>
</div></body>
</html>
Loading

0 comments on commit 0b3bbfd

Please sign in to comment.