|
| 1 | +<?xml version="1.0" encoding="utf-8" ?> |
| 2 | +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
| 3 | +<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en"> |
| 4 | +<head> |
| 5 | +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> |
| 6 | +<meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" /> |
| 7 | +<title>AbPullback.v</title> |
| 8 | +<link rel="stylesheet" href="alectryon.css" type="text/css" /> |
| 9 | +<link rel="stylesheet" href="docutils_basic.css" type="text/css" /> |
| 10 | +<link rel="stylesheet" href="pygments.css" type="text/css" /> |
| 11 | +<script type="text/javascript" src="alectryon.js"></script> |
| 12 | +<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" /> |
| 13 | +<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" /> |
| 14 | +<meta name="viewport" content="width=device-width, initial-scale=1"> |
| 15 | +</head> |
| 16 | +<body> |
| 17 | +<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"> |
| 18 | + |
| 19 | + |
| 20 | +<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">From</span> HoTT <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"> |
| 21 | +</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"> |
| 22 | +</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Export</span> Algebra.Groups.GrpPullback.</span><span class="alectryon-wsp"> |
| 23 | +</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Import</span> Algebra.AbGroups.AbelianGroup.</span><span class="alectryon-wsp"> |
| 24 | +</span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Require Import</span> WildCat.Core.</span><span class="alectryon-wsp"> |
| 25 | +</span></span><span class="alectryon-wsp"> |
| 26 | +</span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Local</span> <span class="kn">Open Scope</span> mc_add_scope.</span><span class="alectryon-wsp"> |
| 27 | +</span></span><span class="alectryon-wsp"> |
| 28 | +<span class="sd">(** * Pullbacks of abelian groups *)</span> |
| 29 | + |
| 30 | +</span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Section</span> <span class="nf">AbPullback</span>.</span><span class="alectryon-wsp"> |
| 31 | +</span></span><span class="alectryon-wsp"> <span class="c">(* Variables are named to correspond with Limits.Pullback. *)</span> |
| 32 | +</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"> |
| 33 | +</span></span><span class="alectryon-wsp"> |
| 34 | +</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">#[export] <span class="kn">Instance</span> <span class="nf">ab_pullback_commutative</span> |
| 35 | + : 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"> |
| 36 | +</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"> |
| 37 | +</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, |
| 38 | +group_sgop x y = group_sgop y x</div></blockquote></div></div></small><span class="alectryon-wsp"> |
| 39 | +</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) = |
| 40 | +group_sgop (d; e; q) (b; c; p)</div></blockquote></div></div></small><span class="alectryon-wsp"> |
| 41 | +</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 : b + d = d + b & |
| 42 | +{q0 : c + e = e + c & |
| 43 | +PathSquare (ap f p0) (ap g q0) |
| 44 | + (grp_homo_op_agree f g p q) |
| 45 | + (grp_homo_op_agree f g q p)}}</div></blockquote></div></div></small><span class="alectryon-wsp"> |
| 46 | +</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)) |
| 47 | + (ap g (commutativity c e)) |
| 48 | + (grp_homo_op_agree f g p q) |
| 49 | + (grp_homo_op_agree f g q p)</div></blockquote></div></div></small><span class="alectryon-wsp"> |
| 50 | +</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_agree f g q p = |
| 51 | +grp_homo_op_agree f g p q @ ap g (commutativity c e)</div></blockquote></div></div></small><span class="alectryon-wsp"> |
| 52 | +</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"> |
| 53 | +</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"> |
| 54 | +</span></span><span class="alectryon-wsp"> |
| 55 | +</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"> |
| 56 | +</span></span><span class="alectryon-wsp"> |
| 57 | + <span class="sd">(** The corecursion principle is inherited from [Group]; use [grp_pullback_corec] and friends from Groups/GrpPullback.v. *)</span> |
| 58 | + |
| 59 | +</span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">End</span> <span class="nf">AbPullback</span>.</span></span></pre> |
| 60 | +</div> |
| 61 | +</div></body> |
| 62 | +</html> |
0 commit comments