Skip to content

Commit

Permalink
index
Browse files Browse the repository at this point in the history
  • Loading branch information
@5HT
5HT committed Aug 5, 2024
1 parent cee9895 commit a8c8842
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 38 deletions.
8 changes: 4 additions & 4 deletions lib/foundations/univalent/path.anders
View file
Original file line number Diff line number Diff line change
Expand Up @@ -359,12 +359,12 @@ def hcomp-Path-is-correct (A : U) (v w : A) (r : I) (u : I → Partial (Path A v

--- Id functions

def transp′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := id A
def transp′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := transp (<i> (ouc p) i) j
def transp′′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := transp (<i> (λ (_ : I), A) i) j
def transp′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := λ (x: A), x
def transp′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := λ (x: A), transp (<i> (ouc p) i) j x
def transp′′′ (A : U) (j : I) (p : (I → U) [j ↦ [(j = 1) → λ (_ : I), A]]) := λ (x: A), transp (<i> (λ (_ : I), A) i) j x

def idfun (A : U) : A → A := λ (a : A), a
def idfun′ (A : U) : A → A := transp (<i> A) 0
def idfun′ (A : U) : A → A := λ (a : A), transp (<i> A) 0 a
def idfun″ (A : U) : A → A := λ (a : A), hcomp A 0 (λ (i : I), []) a

def idfun=idfun′ (A : U) : Path (A → A) (idfun A) (idfun′ A) := <i> transp (<_> A) -i
Expand Down
8 changes: 4 additions & 4 deletions lib/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,18 +26,18 @@
диференціальній геометріїї та в теорії гомотопій. Основи пропонують
фундаментальний базис який використовується для формалізації
сучасної математики в таких системах доведення теорем як: Coq, Agda, Lean.
</p><section><div class="macro"><div class="macro__col"><h3 id="mltt"><b>MLTT</b></h3><ol><li><a href='../foundations/mltt/pi/index.html'>Pi</a>,
</p><section><div class="macro"><div class="macro__col"><h3 id="mltt"><b>Мартіна-Льофа</b></h3><ol><li><a href='../foundations/mltt/pi/index.html'>Pi</a>,
<a href='../foundations/mltt/sigma/index.html'>Sigma</a>,
<a href='../foundations/mltt/id/index.html'>Id</a></li><li><a href='../foundations/mltt/inductive/index.html'>𝟘, 𝟙, 𝟚, W</a></li><li><a href='../foundations/mltt/either/index.html'>Either</a>,
<a href='../foundations/mltt/maybe/index.html'>Maybe</a></li><li><a href='../foundations/mltt/nat/index.html'>ℕ</a>,
<a href='../foundations/mltt/list/index.html'>List</a></li><li><a href='../foundations/mltt/fin/index.html'>Fin<sub>ℕ</sub></a>,
<a href='../foundations/mltt/vec/index.html'>Vec<sub>ℕ</sub></a></li></ol></div><div class="macro__col"><h3 id="univalent"><b>UNIVALENT</b></h3><ol><li><a href="../foundations/univalent/path/index.html">Path</a></li><li><a href="../foundations/univalent/glue/index.html">Glue</a></li><li><a href="../foundations/univalent/equiv/index.html">Equivalence</a></li><li><a href="../foundations/univalent/funext/index.html">Homotopy</a></li><li><a href="../foundations/univalent/iso/index.html">Isomorphism</a></li></ol></div><div class="macro__col"><h3 id="modal"><b>MODAL</b></h3><ol><li><a href="../foundations/modal/modality/index.html">Modality</a></li><li><a href="../foundations/modal/infinitesimal/index.html">Infinitesimal</a></li><li><a href="../foundations/modal/localization/index.html">Localization</a></li><!-- li: a(href='../foundations/modal/process/index.html') Process --></ol></div></div></section><h2>Математики</h2><p>Друга частина базової бібліотеки містить формалізації математичних теорій
<a href='../foundations/mltt/vec/index.html'>Vec<sub>ℕ</sub></a></li></ol></div><div class="macro__col"><h3 id="univalent"><b>Унівалентні</b></h3><ol><li><a href="../foundations/univalent/path/index.html">Path</a></li><li><a href="../foundations/univalent/glue/index.html">Glue</a></li><li><a href="../foundations/univalent/equiv/index.html">Equivalence</a></li><li><a href="../foundations/univalent/funext/index.html">Homotopy</a></li><li><a href="../foundations/univalent/iso/index.html">Isomorphism</a></li></ol></div><div class="macro__col"><h3 id="modal"><b>Модальні</b></h3><ol><li><a href="../foundations/modal/modality/index.html">Modality</a></li><li><a href="../foundations/modal/infinitesimal/index.html">Infinitesimal</a></li><li><a href="../foundations/modal/localization/index.html">Localization</a></li><!-- li: a(href='../foundations/modal/process/index.html') Process --></ol></div></div></section><h2>Математики</h2><p>Друга частина базової бібліотеки містить формалізації математичних теорій
з різних галузей математики: аналіз, алгебра, геометрія, теорія гомотопій,
теорія категорій.
</p><section><div class="macro"><div class="macro__col"><h3 id="categories"><b>ANALYSIS</b></h3><ol><li><a href='../mathematics/analysis/topology/index.html'>Topology</a></li><li><a href='../mathematics/analysis/set/index.html'>Set</a></li><li><a href='../mathematics/analysis/rational/index.html'>ℚ</a>,
</p><section><div class="macro"><div class="macro__col"><h3 id="categories"><b>Аналіз</b></h3><ol><li><a href='../mathematics/analysis/topology/index.html'>Топологія</a></li><li><a href='../mathematics/analysis/set/index.html'>Множини</a></li><li><a href='../mathematics/analysis/rational/index.html'>ℚ</a>,
<a href='../mathematics/analysis/real/index.html'>ℝ</a></li><li><a href='../mathematics/analysis/complex/index.html'>ℂ</a>,
<a href='../mathematics/analysis/quatro/index.html'>ℍ</a>,
<a href='../mathematics/analysis/octo/index.html'>𝕆</a></li></ol></div><div class="macro__col"><h3 id="algebra"><b>ALGEBRA</b></h3><ol><li><a href="../mathematics/algebra/group/index.html">Group</a></li><li><a href="../mathematics/algebra/algebra/index.html">Algebra</a></li><li><a href="../mathematics/algebra/homology/index.html">Homology</a></li></ol></div><div class="macro__col"><h3 id="geometry"><b>GEOMETRY</b></h3><ol><li><a href="../mathematics/geometry/etale/index.html">Etale</a></li><li><a href="../mathematics/geometry/bundle/index.html">Bundle</a></li><li><a href="../mathematics/geometry/manifold/index.html">Manifold</a></li><li><a href="../mathematics/geometry/derham/index.html">de Rham</a></li></ol></div></div></section><section><div class="macro"><div class="macro__col"><h3 id="homotopy"><b>HOMOTOPY</b></h3><ol><li><a href="../mathematics/homotopy/limit/index.html">Limit</a></li><li><a href="../mathematics/homotopy/colimit/index.html">Colimit</a></li><li><a href="../mathematics/homotopy/coeq/index.html">Coequalizer</a></li><li><a href="../mathematics/homotopy/cw/index.html">CW</a></li><li><a href="../mathematics/homotopy/pullback/index.html">Pullback</a></li><li><a href="../mathematics/homotopy/pushout/index.html">Pushout</a></li><li><a href="../mathematics/homotopy/hopf/index.html">Hopf</a></li><li><a href="../mathematics/homotopy/em/index.html">K(G,n)</a></li></ol></div><div class="macro__col"><h3 id="categories"><b>CATEGORIES</b></h3><ol><li><a href="../mathematics/categories/category/index.html">Cagetory</a></li><li><a href="../mathematics/categories/functor/index.html">Functor</a></li><li><a href="../mathematics/categories/groupoid/index.html">Groupoid</a></li><li><a href="../mathematics/categories/presheaf/index.html">Presheaf</a></li><li><a href="../mathematics/categories/topos/index.html">Topos</a></li><li><a href="../mathematics/categories/abelian/index.html">Abelian</a></li></ol></div></div></section><br><p>Базова бібліотека для мови cubicaltt знаходиться на іншій сторінці:
<a href='../mathematics/analysis/octo/index.html'>𝕆</a></li></ol></div><div class="macro__col"><h3 id="algebra"><b>Алгебра</b></h3><ol><li><a href="../mathematics/algebra/group/index.html">Групи</a></li><li><a href="../mathematics/algebra/algebra/index.html">Алгебра</a></li><li><a href="../mathematics/algebra/homology/index.html">Гомології</a></li></ol></div><div class="macro__col"><h3 id="geometry"><b>Геометрія</b></h3><ol><li><a href="../mathematics/geometry/etale/index.html">Етальні</a></li><li><a href="../mathematics/geometry/bundle/index.html">Пучки</a></li><li><a href="../mathematics/geometry/manifold/index.html">Многовиди</a></li><li><a href="../mathematics/geometry/derham/index.html">де Рам</a></li></ol></div></div></section><section><div class="macro"><div class="macro__col"><h3 id="homotopy"><b>Гомотопії</b></h3><ol><li><a href="../mathematics/homotopy/limit/index.html">Ліміти</a></li><li><a href="../mathematics/homotopy/colimit/index.html">Коліміти</a></li><li><a href="../mathematics/homotopy/coeq/index.html">Коеквалайзери</a></li><li><a href="../mathematics/homotopy/cw/index.html">CW-комплекси</a></li><li><a href="../mathematics/homotopy/pullback/index.html">Пулбеки</a></li><li><a href="../mathematics/homotopy/pushout/index.html">Пушаути</a></li><li><a href="../mathematics/homotopy/hopf/index.html">Хопф</a></li><li><a href="../mathematics/homotopy/em/index.html">K(G,n)</a></li></ol></div><div class="macro__col"><h3 id="categories"><b>Категорії</b></h3><ol><li><a href="../mathematics/categories/category/index.html">Категорії</a></li><li><a href="../mathematics/categories/functor/index.html">Функтори</a></li><li><a href="../mathematics/categories/groupoid/index.html">Групоїди</a></li><li><a href="../mathematics/categories/presheaf/index.html">Досніпи</a></li><li><a href="../mathematics/categories/topos/index.html">Топоси</a></li><li><a href="../mathematics/categories/abelian/index.html">Абелеві</a></li></ol></div></div></section><br><p>Базова бібліотека для мови cubicaltt знаходиться на іншій сторінці:
<a href='https://groupoid.space/misc/library/'>Formal Mathematics:
The Cubical Base Library</a><br>
</p></div></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2021&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
60 changes: 30 additions & 30 deletions lib/index.pug
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ block content
section
.macro
.macro__col
h3#mltt <b>MLTT</b>
h3#mltt <b>Мартіна-Льофа</b>
ol
li: <a href='../foundations/mltt/pi/index.html'>Pi</a>,
<a href='../foundations/mltt/sigma/index.html'>Sigma</a>,
Expand All @@ -61,15 +61,15 @@ block content
li: <a href='../foundations/mltt/fin/index.html'>Fin<sub>ℕ</sub></a>,
<a href='../foundations/mltt/vec/index.html'>Vec<sub>ℕ</sub></a>
.macro__col
h3#univalent <b>UNIVALENT</b>
h3#univalent <b>Унівалентні</b>
ol
li: a(href='../foundations/univalent/path/index.html') Path
li: a(href='../foundations/univalent/glue/index.html') Glue
li: a(href='../foundations/univalent/equiv/index.html') Equivalence
li: a(href='../foundations/univalent/funext/index.html') Homotopy
li: a(href='../foundations/univalent/iso/index.html') Isomorphism
.macro__col
h3#modal <b>MODAL</b>
h3#modal <b>Модальні</b>
ol
li: a(href='../foundations/modal/modality/index.html') Modality
li: a(href='../foundations/modal/infinitesimal/index.html') Infinitesimal
Expand All @@ -85,50 +85,50 @@ block content
section
.macro
.macro__col
h3#categories <b>ANALYSIS</b>
h3#categories <b>Аналіз</b>
ol
li: <a href='../mathematics/analysis/topology/index.html'>Topology</a>
li: <a href='../mathematics/analysis/set/index.html'>Set</a>
li: <a href='../mathematics/analysis/topology/index.html'>Топологія</a>
li: <a href='../mathematics/analysis/set/index.html'>Множини</a>
li: <a href='../mathematics/analysis/rational/index.html'>ℚ</a>,
<a href='../mathematics/analysis/real/index.html'>ℝ</a>
li: <a href='../mathematics/analysis/complex/index.html'>ℂ</a>,
<a href='../mathematics/analysis/quatro/index.html'>ℍ</a>,
<a href='../mathematics/analysis/octo/index.html'>𝕆</a>
.macro__col
h3#algebra <b>ALGEBRA</b>
h3#algebra <b>Алгебра</b>
ol
li: a(href='../mathematics/algebra/group/index.html') Group
li: a(href='../mathematics/algebra/algebra/index.html') Algebra
li: a(href='../mathematics/algebra/homology/index.html') Homology
li: a(href='../mathematics/algebra/group/index.html') Групи
li: a(href='../mathematics/algebra/algebra/index.html') Алгебра
li: a(href='../mathematics/algebra/homology/index.html') Гомології
.macro__col
h3#geometry <b>GEOMETRY</b>
h3#geometry <b>Геометрія</b>
ol
li: a(href='../mathematics/geometry/etale/index.html') Etale
li: a(href='../mathematics/geometry/bundle/index.html') Bundle
li: a(href='../mathematics/geometry/manifold/index.html') Manifold
li: a(href='../mathematics/geometry/derham/index.html') de Rham
li: a(href='../mathematics/geometry/etale/index.html') Етальні
li: a(href='../mathematics/geometry/bundle/index.html') Пучки
li: a(href='../mathematics/geometry/manifold/index.html') Многовиди
li: a(href='../mathematics/geometry/derham/index.html') де Рам
section
.macro
.macro__col
h3#homotopy <b>HOMOTOPY</b>
h3#homotopy <b>Гомотопії</b>
ol
li: a(href='../mathematics/homotopy/limit/index.html') Limit
li: a(href='../mathematics/homotopy/colimit/index.html') Colimit
li: a(href='../mathematics/homotopy/coeq/index.html') Coequalizer
li: a(href='../mathematics/homotopy/cw/index.html') CW
li: a(href='../mathematics/homotopy/pullback/index.html') Pullback
li: a(href='../mathematics/homotopy/pushout/index.html') Pushout
li: a(href='../mathematics/homotopy/hopf/index.html') Hopf
li: a(href='../mathematics/homotopy/limit/index.html') Ліміти
li: a(href='../mathematics/homotopy/colimit/index.html') Коліміти
li: a(href='../mathematics/homotopy/coeq/index.html') Коеквалайзери
li: a(href='../mathematics/homotopy/cw/index.html') CW-комплекси
li: a(href='../mathematics/homotopy/pullback/index.html') Пулбеки
li: a(href='../mathematics/homotopy/pushout/index.html') Пушаути
li: a(href='../mathematics/homotopy/hopf/index.html') Хопф
li: a(href='../mathematics/homotopy/em/index.html') K(G,n)
.macro__col
h3#categories <b>CATEGORIES</b>
h3#categories <b>Категорії</b>
ol
li: a(href='../mathematics/categories/category/index.html') Cagetory
li: a(href='../mathematics/categories/functor/index.html') Functor
li: a(href='../mathematics/categories/groupoid/index.html') Groupoid
li: a(href='../mathematics/categories/presheaf/index.html') Presheaf
li: a(href='../mathematics/categories/topos/index.html') Topos
li: a(href='../mathematics/categories/abelian/index.html') Abelian
li: a(href='../mathematics/categories/category/index.html') Категорії
li: a(href='../mathematics/categories/functor/index.html') Функтори
li: a(href='../mathematics/categories/groupoid/index.html') Групоїди
li: a(href='../mathematics/categories/presheaf/index.html') Досніпи
li: a(href='../mathematics/categories/topos/index.html') Топоси
li: a(href='../mathematics/categories/abelian/index.html') Абелеві
br.
p.
Базова бібліотека для мови cubicaltt знаходиться на іншій сторінці:
Expand Down

0 comments on commit a8c8842

Please sign in to comment.