-
Notifications
You must be signed in to change notification settings - Fork 193
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 @ 36b5e8b 🚀
- Loading branch information
0 parents
commit 3bf05a3
Showing
2,506 changed files
with
1,601,526 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.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
733 changes: 733 additions & 0 deletions
733
alectryon-html/HoTT.Algebra.AbGroups.Abelianization.html
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
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,41 @@ | ||
| <?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>AbGroups.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="tango_subtle.css" type="text/css" /> | ||
| <link rel="stylesheet" href="tango_subtle.min.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.17.0+0.17.0. 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"><!-- Generator: Alectryon --><span class="alectryon-wsp"><span class="highlight"><span class="sd">(** Theory *)</span> | ||
|
|
||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.Groups.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.AbelianGroup.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.Abelianization.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.AbPullback.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.AbPushout.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.Biproduct.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.AbHom.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.Cyclic.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.Centralizer.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| <span class="c">(* The theory of Ext groups of abelian groups is in HoTT.Algebra.AbSES. *)</span> | ||
|
|
||
| <span class="sd">(** Examples *)</span> | ||
|
|
||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> HoTT.Algebra.AbGroups.Z.</span></span></span></pre> | ||
| </div> | ||
| </div></body> | ||
| </html> |
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
Large diffs are not rendered by default.
Oops, something went wrong.
1,964 changes: 1,964 additions & 0 deletions
1,964
alectryon-html/HoTT.Algebra.AbSES.PullbackFiberSequence.html
Large diffs are not rendered by default.
Oops, something went wrong.
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,31 @@ | ||
| <?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>AbSES.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="tango_subtle.css" type="text/css" /> | ||
| <link rel="stylesheet" href="tango_subtle.min.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.17.0+0.17.0. 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"><!-- Generator: Alectryon --><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.Core.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.Ext.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.Pullback.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.PullbackFiberSequence.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.Pushout.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.BaerSum.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.DirectSum.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Export</span> AbSES.SixTerm.</span></span></span></pre> | ||
| </div> | ||
| </div></body> | ||
| </html> |
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,37 @@ | ||
| <?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>Aut.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="tango_subtle.css" type="text/css" /> | ||
| <link rel="stylesheet" href="tango_subtle.min.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.17.0+0.17.0. 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"><!-- Generator: Alectryon --><span class="alectryon-wsp"><span class="highlight"><span class="c">(* -*- mode: coq; mode: visual-line -*- *)</span> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Basics.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Truncations.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Algebra.ooGroup.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Spaces.BAut.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Pointed.Core.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Local Open Scope</span> pointed_scope.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| <span class="sd">(** * Automorphism oo-Groups *)</span> | ||
|
|
||
| <span class="sd">(** We define [Aut X] using the pointed, connected type [BAut X]. *)</span> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">Aut</span> (<span class="nv">X</span> : <span class="kt">Type</span>) : ooGroup | ||
| := Build_ooGroup [BAut X, _] _.</span></span></span></pre> | ||
| </div> | ||
| </div></body> | ||
| </html> |
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,34 @@ | ||
| <?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>Congruence.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="tango_subtle.css" type="text/css" /> | ||
| <link rel="stylesheet" href="tango_subtle.min.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.17.0+0.17.0. 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"><!-- Generator: Alectryon --><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Require Import</span> Classes.interfaces.abstract_algebra.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| <span class="c">(* We say that a relation is a congruence if it respects the operation.</span> | ||
| <span class="c"> This is technically incorrect since we are not enforcing the relation to be an equivalence relation.</span> | ||
| <span class="c">*)</span> | ||
|
|
||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Local Open Scope</span> mc_mult_scope.</span></span><span class="alectryon-wsp"> | ||
| </span></span><span class="alectryon-wsp"><span class="highlight"> | ||
| </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="highlight"><span class="kn">Class</span> <span class="nf">IsCongruence</span> {<span class="nv">G</span>} `{SgOp G} (R : Relation G) := { | ||
| iscong {x x' y y'} : R x x' -> R y y' -> R (x * y) (x' * y'); | ||
| }.</span></span></span></pre> | ||
| </div> | ||
| </div></body> | ||
| </html> |
Oops, something went wrong.