Code

Simplicial Type Theory#1118

Code

Closed

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

  Copy full SHA for eb9f3e6

• The directed relation on the directed interval type

  fredrik-bakke

  committed
  7b8a548

  Copy full SHA for 7b8a548

• standard simplicial cubes

  fredrik-bakke

  committed
  db3b59a

  Copy full SHA for db3b59a

• Simplicial arrows

  fredrik-bakke

  committed
  c6b8d8e

  Copy full SHA for c6b8d8e

• simplicial edges

  fredrik-bakke

  committed
  db2f1bb

  Copy full SHA for db2f1bb

• _→₂_ notation simplicial edges

  fredrik-bakke

  committed
  692f30a

  Copy full SHA for 692f30a

• The action on simplicial edges of functions

  fredrik-bakke

  committed
  146189d

  Copy full SHA for 146189d

• Simplicial natural transformations

  fredrik-bakke

  committed
  cbb0a42

  Copy full SHA for cbb0a42

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

  fredrik-bakke

  committed
  cda98ba

  Copy full SHA for cda98ba

• Horizontal composition of simplicial arrows of functions

  fredrik-bakke

  committed
  ecd606e

  Copy full SHA for ecd606e

• Horizontal composition of simplicial edges between functions

  fredrik-bakke

  committed
  1c71fe4

  Copy full SHA for 1c71fe4

• Whiskering operations on simplicial arrows of functions

  fredrik-bakke

  committed
  b4ac7e4

  Copy full SHA for b4ac7e4

Commits on Apr 18, 2024

• Whiskering operations on simplicial edges between functions

  fredrik-bakke

  committed
  a2e82f2

  Copy full SHA for a2e82f2

• inline (leq|Id)-2-Prop

  fredrik-bakke

  committed
  f439a35

  Copy full SHA for f439a35

• The boundary of the standard simplicial cube

  fredrik-bakke

  committed
  b5b9067

  Copy full SHA for b5b9067

• WIP 2-simplices

  fredrik-bakke

  committed
  44e8ef7

  Copy full SHA for 44e8ef7

• comma types

  fredrik-bakke

  committed
  e6e6a16

  Copy full SHA for e6e6a16

Commits on Apr 19, 2024

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

  fredrik-bakke

  authored
  e7c473a

  Copy full SHA for e7c473a

Commits on Apr 22, 2024

• action on simplicial edges of dependent functions

  fredrik-bakke

  committed
  3b869d3

  Copy full SHA for 3b869d3

• some work

  fredrik-bakke

  committed
  a64843d

  Copy full SHA for a64843d

• dependent simplicial edges

  fredrik-bakke

  committed
  5d733e1

  Copy full SHA for 5d733e1

• Characterizing equality of dependent simplicial edges over a fixed edge

  fredrik-bakke

  committed
  938888e

  Copy full SHA for 938888e

Commits on Apr 23, 2024

• free directed loops

  fredrik-bakke

  committed
  c373277

  Copy full SHA for c373277

• The universal property of the directed circle

  fredrik-bakke

  committed
  0ce1e43

  Copy full SHA for 0ce1e43

• the directed circle

  fredrik-bakke

  committed
  897cf05

  Copy full SHA for 897cf05

• rewritinf rules for the directed circle

  fredrik-bakke

  committed
  df77481

  Copy full SHA for df77481

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

  fredrik-bakke

  authored
  866ff56

  Copy full SHA for 866ff56

• fix links

  fredrik-bakke

  committed
  c3c1464

  Copy full SHA for c3c1464

• negated equality universal-cover-circle

  fredrik-bakke

  committed
  a43ed06

  Copy full SHA for a43ed06

• pre-commit

  fredrik-bakke

  committed
  8084b1d

  Copy full SHA for 8084b1d

• The loop of the circle is nontrivial

  fredrik-bakke

  committed
  fc9641e

  Copy full SHA for fc9641e

Commits on Apr 24, 2024

• simplicially discrete types

  fredrik-bakke

  committed
  0f14dc1

  Copy full SHA for 0f14dc1

• a space

  fredrik-bakke

  committed
  997c85f

  Copy full SHA for 997c85f

Commits on Apr 25, 2024

• duality postcomposition pullbacks <-> pullback property pushouts

  fredrik-bakke

  committed
  92e41f2

  Copy full SHA for 92e41f2

• Simplicial mapping cylinders

  fredrik-bakke

  committed
  804d5fa

  Copy full SHA for 804d5fa

• nit foundation

  fredrik-bakke

  committed
  0202ce2

  Copy full SHA for 0202ce2

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

  fredrik-bakke

  authored
  16759ec

  Copy full SHA for 16759ec

Commits on Apr 29, 2024

• fixes pushout-products

  fredrik-bakke

  committed
  ff4d2da

  Copy full SHA for ff4d2da

• propositions are local at inhabited types

  fredrik-bakke

  committed
  9582b53

  Copy full SHA for 9582b53

• todos orthogonal maps

  fredrik-bakke

  committed
  0b31700

  Copy full SHA for 0b31700

• Constant free directed loops

  fredrik-bakke

  committed
  e91338a

  Copy full SHA for e91338a

• standard simplicial joins

  fredrik-bakke

  committed
  9f1dcd1

  Copy full SHA for 9f1dcd1

• wip directed circle

  fredrik-bakke

  committed
  2c3cee6

  Copy full SHA for 2c3cee6

• the representing arrow and directed edge

  fredrik-bakke

  committed
  2aa05f4

  Copy full SHA for 2aa05f4

• informal definition simplicial suspension

  fredrik-bakke

  committed
  6b31f75

  Copy full SHA for 6b31f75

• small fixes comma types

  fredrik-bakke

  committed
  09a0edf

  Copy full SHA for 09a0edf

• two easy examples of simplicially discrete types

  fredrik-bakke

  committed
  d1dd5a5

  Copy full SHA for d1dd5a5

• simplicial cones

  fredrik-bakke

  committed
  750c2c8

  Copy full SHA for 750c2c8

• informal definition simplicial spine

  fredrik-bakke

  committed
  aa47a4e

  Copy full SHA for aa47a4e

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

  fredrik-bakke

  authored
  e9c3c2a

  Copy full SHA for e9c3c2a

• rename directed relation module

  fredrik-bakke

  committed
  20380d0

  Copy full SHA for 20380d0

• "simplicial edge" -> "directed edge"

  fredrik-bakke

  committed
  59d064d

  Copy full SHA for 59d064d

• pre-commit

  fredrik-bakke

  committed
  679ca2e

  Copy full SHA for 679ca2e

• add reference RS17

  fredrik-bakke

  committed
  7a866bb

  Copy full SHA for 7a866bb

Commits on Apr 30, 2024

• small fixes

  fredrik-bakke

  committed
  cd2cce9

  Copy full SHA for cd2cce9

Commits on May 1, 2024

• simplicially covariant type families

  fredrik-bakke

  committed
  2b9f23b

  Copy full SHA for 2b9f23b

Commits on May 2, 2024

• the directed interval is not 0-connected

  fredrik-bakke

  committed
  a23f1a7

  Copy full SHA for a23f1a7

• strengthen The directed interval is not connected

  fredrik-bakke

  committed
  d6521a1

  Copy full SHA for d6521a1

• strengthen The directed interval is not connected

  fredrik-bakke

  committed
  2c28378

  Copy full SHA for 2c28378

Commits on May 6, 2024

• max and min operators on directed interval

  fredrik-bakke

  committed
  943e474

  Copy full SHA for 943e474

• prose fixes erasing-equality

  fredrik-bakke

  committed
  151319e

  Copy full SHA for 151319e

• add --confluence-check flag

  fredrik-bakke

  committed
  e77ca01

  Copy full SHA for e77ca01

• fix rewriting-directed-circle

  fredrik-bakke

  committed
  66fab80

  Copy full SHA for 66fab80

• fix rewriting-directed-circle

  fredrik-bakke

  committed
  f0780ab

  Copy full SHA for f0780ab

Commits on May 21, 2024

• some nicer type setting

  fredrik-bakke

  committed
  1984294

  Copy full SHA for 1984294

Commits on Jun 1, 2024

• define Simplicially fully-faithful maps

  fredrik-bakke

  committed
  edb5321

  Copy full SHA for edb5321

Commits on Jun 3, 2024

• add reference MR23b

  fredrik-bakke

  committed
  172f593

  Copy full SHA for 172f593

• some work on logic

  fredrik-bakke

  committed
  2ade64e

  Copy full SHA for 2ade64e

• more characterizations of directed edges

  fredrik-bakke

  committed
  19503fa

  Copy full SHA for 19503fa

• two corollaries for simplicially discrete types

  fredrik-bakke

  committed
  5270b4f

  Copy full SHA for 5270b4f

• pre-commit

  fredrik-bakke

  committed
  0c9503e

  Copy full SHA for 0c9503e

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

  fredrik-bakke

  committed
  aeb48db

  Copy full SHA for aeb48db

• globularly coskeletal types

  fredrik-bakke

  committed
  b777ffb

  Copy full SHA for b777ffb

• a remark on standard simplices

  fredrik-bakke

  committed
  5a52a0d

  Copy full SHA for 5a52a0d

• incomplete proof loop of directed circle is nontrivial

  fredrik-bakke

  committed
  6797c80

  Copy full SHA for 6797c80

• line wrap

  fredrik-bakke

  committed
  a6324af

  Copy full SHA for a6324af

• rename relation to inequality directed interval type

  fredrik-bakke

  committed
  b90a040

  Copy full SHA for b90a040

• wip simplicial spines

  fredrik-bakke

  committed
  73da6cb

  Copy full SHA for 73da6cb

• wip directed edges in the booleans

  fredrik-bakke

  committed
  78453f4

  Copy full SHA for 78453f4

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

  fredrik-bakke

  authored
  025ef51

  Copy full SHA for 025ef51

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

  fredrik-bakke

  committed
  cfe7eda

  Copy full SHA for cfe7eda

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

  fredrik-bakke

  committed
  7600f0e

  Copy full SHA for 7600f0e

Commits on Jun 4, 2024

• is-orthogonal-htpy

  fredrik-bakke

  committed
  10930ef

  Copy full SHA for 10930ef

• The canonical projection from a coproduct to the booleans

  fredrik-bakke

  committed
  fb4ef17

  Copy full SHA for fb4ef17

• closure properties of null maps

  fredrik-bakke

  committed
  d3fec69

  Copy full SHA for d3fec69

• a remark on null types

  fredrik-bakke

  committed
  3b9464f

  Copy full SHA for 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

  Copy full SHA for 51536e0

• characterizing directed edges in the booleans

  fredrik-bakke

  committed
  2d99de8

  Copy full SHA for 2d99de8

• some fixes

  fredrik-bakke

  committed
  3a6b62d

  Copy full SHA for 3a6b62d

• rename coskeletal to globularly coskeletal

  fredrik-bakke

  committed
  3e6ec97

  Copy full SHA for 3e6ec97

• factor out coproducts of null types

  fredrik-bakke

  committed
  cfcf354

  Copy full SHA for cfcf354

• The hom-types of a truncated type are truncated

  fredrik-bakke

  committed
  c8571f1

  Copy full SHA for c8571f1

Commits on Jun 5, 2024

• work

  fredrik-bakke

  committed
  807ac8d

  Copy full SHA for 807ac8d

Commits on Jun 12, 2024

• idk

  fredrik-bakke

  committed
  406223f

  Copy full SHA for 406223f

Commits on Sep 17, 2024

• wip stt

  fredrik-bakke

  committed
  913e3dd

  Copy full SHA for 913e3dd

Commits on Sep 18, 2024

• Base change of sections

  fredrik-bakke

  committed
  a41e0fb

  Copy full SHA for a41e0fb

Commits on Sep 19, 2024

• informal proof Retracts of transposing adjunctions

  fredrik-bakke

  committed
  87a679f

  Copy full SHA for 87a679f

• delete irrelevant code transposing adjunctions

  fredrik-bakke

  committed
  4b5c48d

  Copy full SHA for 4b5c48d

Commits on Sep 21, 2024

• more stuff transposing adjunctions

  fredrik-bakke

  committed
  e50e71c

  Copy full SHA for e50e71c

Commits on Oct 3, 2024

• typo horizontal comp directed edges functions

  fredrik-bakke

  committed
  a74eebd

  Copy full SHA for a74eebd

• change notation natural transformations

  fredrik-bakke

  committed
  6515a65

  Copy full SHA for 6515a65

• horizontal composition natural transformations

  fredrik-bakke

  committed
  6ef3dd6

  Copy full SHA for 6ef3dd6

• additions adjunctions

  fredrik-bakke

  committed
  52e0f32

  Copy full SHA for 52e0f32

• late onset pre-commit

  fredrik-bakke

  committed
  2ba7ff9

  Copy full SHA for 2ba7ff9

• wip normed maps

  fredrik-bakke

  committed
  8ab0737

  Copy full SHA for 8ab0737