-
Notifications
You must be signed in to change notification settings - Fork 187
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ b1ace5a 🚀
- Loading branch information
0 parents
commit 2cb254c
Showing
2,609 changed files
with
1,649,690 additions
and
0 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,83 @@ | ||
| <?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.18.0+0.18.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 $-> A) (<span class="nv">g</span> : C $-> 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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 & | ||
| {q0 : sg_op c e = sg_op e c & | ||
| PathSquare (ap f p0) (ap g q0) | ||
| ((grp_homo_op f b d @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f b) y) q @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g e)) p)) @ | ||
| (grp_homo_op g c e)^) | ||
| ((grp_homo_op f d b @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f d) y) p @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g c)) q)) @ | ||
| (grp_homo_op g e c)^)}}</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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 f b d @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f b) y) q @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g e)) p)) @ | ||
| (grp_homo_op g c e)^) | ||
| ((grp_homo_op f d b @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f d) y) p @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g c)) q)) @ | ||
| (grp_homo_op g e c)^)</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 $-> A</span></span></span><br><span><var>g</var><span class="hyp-type"><b>: </b><span>C $-> 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 f d b @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f d) y) p @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g c)) q)) @ | ||
| (grp_homo_op g e c)^) = | ||
| ((grp_homo_op f b d @ | ||
| (ap (<span class="kr">fun</span> <span class="nv">y</span> : A => sg_op (f b) y) q @ | ||
| ap (<span class="kr">fun</span> <span class="nv">x</span> : A => sg_op x (g e)) p)) @ | ||
| (grp_homo_op g c e)^) @ 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> |
Oops, something went wrong.