Code

Simplicial Type Theory#1118

Code

Draft

fredrik-bakke wants to merge 105 commits intoUniMath:masterUniMath/agda-unimath:masterfrom fredrik-bakke:simplicial-type-theoryfredrik-bakke/agda-unimath:simplicial-type-theoryCopy head branch name to clipboard

+10,383-102

Commits

Commits on Apr 17, 2024

• the directed interval type

  fredrik-bakke

  committed
  eb9f3e6

• The directed relation on the directed interval type

  fredrik-bakke

  committed
  7b8a548

• standard simplicial cubes

  fredrik-bakke

  committed
  db3b59a

• Simplicial arrows

  fredrik-bakke

  committed
  c6b8d8e

• simplicial edges

  fredrik-bakke

  committed
  db2f1bb

• _→₂_ notation simplicial edges

  fredrik-bakke

  committed
  692f30a

• The action on simplicial edges of functions

  fredrik-bakke

  committed
  146189d

• Simplicial natural transformations

  fredrik-bakke

  committed
  cbb0a42

• The canonical inclusion of the booleans into the directed interval is an embedding

  fredrik-bakke

  committed
  cda98ba

• Horizontal composition of simplicial arrows of functions

  fredrik-bakke

  committed
  ecd606e

• Horizontal composition of simplicial edges between functions

  fredrik-bakke

  committed
  1c71fe4

• Whiskering operations on simplicial arrows of functions

  fredrik-bakke

  committed
  b4ac7e4

Commits on Apr 18, 2024

• Whiskering operations on simplicial edges between functions

  fredrik-bakke

  committed
  a2e82f2

• inline (leq|Id)-2-Prop

  fredrik-bakke

  committed
  f439a35

• The boundary of the standard simplicial cube

  fredrik-bakke

  committed
  b5b9067

• WIP 2-simplices

  fredrik-bakke

  committed
  44e8ef7

• comma types

  fredrik-bakke

  committed
  e6e6a16

Commits on Apr 19, 2024

• Merge branch 'master' into simplicial-type-theory

  fredrik-bakke

  authored
  e7c473a

Commits on Apr 22, 2024

• action on simplicial edges of dependent functions

  fredrik-bakke

  committed
  3b869d3

• some work

  fredrik-bakke

  committed
  a64843d

• dependent simplicial edges

  fredrik-bakke

  committed
  5d733e1

• Characterizing equality of dependent simplicial edges over a fixed edge

  fredrik-bakke

  committed
  938888e

Commits on Apr 23, 2024

• free directed loops

  fredrik-bakke

  committed
  c373277

• The universal property of the directed circle

  fredrik-bakke

  committed
  0ce1e43

• the directed circle

  fredrik-bakke

  committed
  897cf05

• rewritinf rules for the directed circle

  fredrik-bakke

  committed
  df77481

• Merge branch 'master' into simplicial-type-theory

  fredrik-bakke

  authored
  866ff56

• fix links

  fredrik-bakke

  committed
  c3c1464

• negated equality universal-cover-circle

  fredrik-bakke

  committed
  a43ed06

• pre-commit

  fredrik-bakke

  committed
  8084b1d

• The loop of the circle is nontrivial

  fredrik-bakke

  committed
  fc9641e

Commits on Apr 24, 2024

• simplicially discrete types

  fredrik-bakke

  committed
  0f14dc1

• a space

  fredrik-bakke

  committed
  997c85f

Commits on Apr 25, 2024

• duality postcomposition pullbacks <-> pullback property pushouts

  fredrik-bakke

  committed
  92e41f2

• Simplicial mapping cylinders

  fredrik-bakke

  committed
  804d5fa

• nit foundation

  fredrik-bakke

  committed
  0202ce2

• Merge branch 'master' into simplicial-type-theory

  fredrik-bakke

  authored
  16759ec

Commits on Apr 29, 2024

• fixes pushout-products

  fredrik-bakke

  committed
  ff4d2da

• propositions are local at inhabited types

  fredrik-bakke

  committed
  9582b53

• todos orthogonal maps

  fredrik-bakke

  committed
  0b31700

• Constant free directed loops

  fredrik-bakke

  committed
  e91338a

• standard simplicial joins

  fredrik-bakke

  committed
  9f1dcd1

• wip directed circle

  fredrik-bakke

  committed
  2c3cee6

• the representing arrow and directed edge

  fredrik-bakke

  committed
  2aa05f4

• informal definition simplicial suspension

  fredrik-bakke

  committed
  6b31f75

• small fixes comma types

  fredrik-bakke

  committed
  09a0edf

• two easy examples of simplicially discrete types

  fredrik-bakke

  committed
  d1dd5a5

• simplicial cones

  fredrik-bakke

  committed
  750c2c8

• informal definition simplicial spine

  fredrik-bakke

  committed
  aa47a4e

• Merge branch 'master' into simplicial-type-theory

  fredrik-bakke

  authored
  e9c3c2a

• rename directed relation module

  fredrik-bakke

  committed
  20380d0

• "simplicial edge" -> "directed edge"

  fredrik-bakke

  committed
  59d064d

• pre-commit

  fredrik-bakke

  committed
  679ca2e

• add reference RS17

  fredrik-bakke

  committed
  7a866bb

Commits on Apr 30, 2024

• small fixes

  fredrik-bakke

  committed
  cd2cce9

Commits on May 1, 2024

• simplicially covariant type families

  fredrik-bakke

  committed
  2b9f23b

Commits on May 2, 2024

• the directed interval is not 0-connected

  fredrik-bakke

  committed
  a23f1a7

• strengthen The directed interval is not connected

  fredrik-bakke

  committed
  d6521a1

• strengthen The directed interval is not connected

  fredrik-bakke

  committed
  2c28378

Commits on May 6, 2024

• max and min operators on directed interval

  fredrik-bakke

  committed
  943e474

• prose fixes erasing-equality

  fredrik-bakke

  committed
  151319e

• add --confluence-check flag

  fredrik-bakke

  committed
  e77ca01

• fix rewriting-directed-circle

  fredrik-bakke

  committed
  66fab80

• fix rewriting-directed-circle

  fredrik-bakke

  committed
  f0780ab

Commits on May 21, 2024

• some nicer type setting

  fredrik-bakke

  committed
  1984294

Commits on Jun 1, 2024

• define Simplicially fully-faithful maps

  fredrik-bakke

  committed
  edb5321

Commits on Jun 3, 2024

• add reference MR23b

  fredrik-bakke

  committed
  172f593

• some work on logic

  fredrik-bakke

  committed
  2ade64e

• more characterizations of directed edges

  fredrik-bakke

  committed
  19503fa

• two corollaries for simplicially discrete types

  fredrik-bakke

  committed
  5270b4f

• pre-commit

  fredrik-bakke

  committed
  0c9503e

• detailed analysis of the image factorization of bool -> 𝟚

  fredrik-bakke

  committed
  aeb48db

• globularly coskeletal types

  fredrik-bakke

  committed
  b777ffb

• a remark on standard simplices

  fredrik-bakke

  committed
  5a52a0d

• incomplete proof loop of directed circle is nontrivial

  fredrik-bakke

  committed
  6797c80

• line wrap

  fredrik-bakke

  committed
  a6324af

• rename relation to inequality directed interval type

  fredrik-bakke

  committed
  b90a040

• wip simplicial spines

  fredrik-bakke

  committed
  73da6cb

• wip directed edges in the booleans

  fredrik-bakke

  committed
  78453f4

• Merge branch 'master' into simplicial-type-theory

  fredrik-bakke

  authored
  025ef51

• null types are closed under Pi, exponentials, products and Sigma

  fredrik-bakke

  committed
  cfe7eda

• simplicially discrete types are closed under Pi, exponentials, products and Sigma

  fredrik-bakke

  committed
  7600f0e

Commits on Jun 4, 2024

• is-orthogonal-htpy

  fredrik-bakke

  committed
  10930ef

• The canonical projection from a coproduct to the booleans

  fredrik-bakke

  committed
  fb4ef17

• closure properties of null maps

  fredrik-bakke

  committed
  d3fec69

• a remark on null types

  fredrik-bakke

  committed
  3b9464f

• A family over a simplicially discrete type is a family of simplicially discrete types if and only if the dependent sum is

  fredrik-bakke

  committed
  51536e0

• characterizing directed edges in the booleans

  fredrik-bakke

  committed
  2d99de8

• some fixes

  fredrik-bakke

  committed
  3a6b62d

• rename coskeletal to globularly coskeletal

  fredrik-bakke

  committed
  3e6ec97

• factor out coproducts of null types

  fredrik-bakke

  committed
  cfcf354

• The hom-types of a truncated type are truncated

  fredrik-bakke

  committed
  c8571f1

Commits on Jun 5, 2024

• work

  fredrik-bakke

  committed
  807ac8d

Commits on Jun 12, 2024

• idk

  fredrik-bakke

  committed
  406223f

Commits on Sep 17, 2024

• wip stt

  fredrik-bakke

  committed
  913e3dd

Commits on Sep 18, 2024

• Base change of sections

  fredrik-bakke

  committed
  a41e0fb

Commits on Sep 19, 2024

• informal proof Retracts of transposing adjunctions

  fredrik-bakke

  committed
  87a679f

• delete irrelevant code transposing adjunctions

  fredrik-bakke

  committed
  4b5c48d

Commits on Sep 21, 2024

• more stuff transposing adjunctions

  fredrik-bakke

  committed
  e50e71c

Commits on Oct 3, 2024

• typo horizontal comp directed edges functions

  fredrik-bakke

  committed
  a74eebd

• change notation natural transformations

  fredrik-bakke

  committed
  6515a65

• horizontal composition natural transformations

  fredrik-bakke

  committed
  6ef3dd6

• additions adjunctions

  fredrik-bakke

  committed
  52e0f32

• late onset pre-commit

  fredrik-bakke

  committed
  2ba7ff9

• wip normed maps

  fredrik-bakke

  committed
  8ab0737