UniMath/SymmetryBook

Issues

• Remark 4.2.21, universes

  #198 opened 7 months ago by marcbezem
  4

• Can an object be considered the same if we change its type?

  #196 opened a year ago by marcbezem
  0

• Lemma 2.15.4 (6)

  #162 opened 2 years ago by marcbezem
  7

• 2.22.10-13

  #163 opened 2 years ago by marcbezem
  5

• introduce quotient sets by means of a higher inductive type

  #166 opened 2 years ago by DanGrayson
  6

• 2.24.2-4

  #164 opened 2 years ago by marcbezem
  2

• 2.12.8-10

  #165 opened 2 years ago by marcbezem
  1

• Last paragraph of 2.16

  #167 opened 2 years ago by marcbezem
  9

• Building of book fails

  #179 opened 2 years ago by benediktahrens
  6

• Definition and use of \ne (aka \neq)

  #168 opened 2 years ago by marcbezem
  4

• Theorem 2.26.4

  #172 opened 2 years ago by marcbezem
  4

• universal set bundle

  #187 opened 2 years ago by marcbezem
  7

• Commutativity of diagrams

  #183 opened 2 years ago by marcbezem
  16

• Footnote 66 explaining the first ! (bang)

  #175 opened 2 years ago by marcbezem
  4

• "ad" is not defined

  #194 opened 2 years ago by ncfavier
  1

• Higher deloopings of abelian groups

  #193 opened 2 years ago by UlrikBuchholtz
  0

• Potential inconsistency in coproduct notation

  #189 opened 2 years ago by fizruk
  0

• The concept of homotopy type

  #185 opened 2 years ago by marcbezem
  2

• Definition of transitive G-set

  #184 opened 2 years ago by pierrecagne
  7

• Subscripts to \eqto

  #182 opened 2 years ago by marcbezem
  2

• Injection/inclusion in Propositional Resizing 2.18.6, or rather just "map"?

  #177 opened 2 years ago by marcbezem
  14

• Build problem

  #178 opened 2 years ago by benediktahrens
  1

• Rings and abstract rings

  #176 opened 2 years ago
  0

• garbled text

  #160 opened 2 years ago by DanGrayson
  0

• Introduce the subset notation

  #174 opened 2 years ago by UlrikBuchholtz
  4

• image inclusion

  #171 opened 2 years ago by marcbezem
  4

• Expand App. B.1 to discuss principles compatible with decidable equality and program extraction

  #173 opened 2 years ago by UlrikBuchholtz
  0

• Changing all xymatrix diagrams to tikzcd

  #169 opened 2 years ago by favonia
  3

• Moratorium on new global changes?

  #161 opened 2 years ago by marcbezem
  1

• Identity crisis

  #159 opened 2 years ago by marcbezem
  3

• definitions

  #157 opened 2 years ago by DanGrayson
  5

• Homotopy initiality vs higher induction

  #158 opened 2 years ago
  1

• Proof of Cauchy's theorem 7.3.2

  #156 opened 2 years ago by pcapriotti
  4

• \equiv

  #145 opened 3 years ago by DanGrayson
  13

• Theorem 3.1.2

  #153 opened 3 years ago by DanGrayson
  9

• diagrams

  #155 opened 3 years ago by DanGrayson
  1

• chapter 3

  #154 opened 3 years ago by DanGrayson
  0

• subtypes

  #152 opened 3 years ago by DanGrayson
  1

• Notation for total space of family of types

  #150 opened 3 years ago by marcbezem
  3

• " merely "

  #151 opened 3 years ago by DanGrayson
  2

• "merely"

  #148 opened 3 years ago by DanGrayson
  5

• isnType

  #147 opened 3 years ago by DanGrayson
  0

• n-truncation

  #146 opened 3 years ago by UlrikBuchholtz
  1

• Definition of ordered field and real numbers

  #143 opened 3 years ago
  1

• Scope of chapter 8

  #141 opened 3 years ago
  1

• Definition of Pythagorean fields

  #140 opened 3 years ago
  5

• Sign homomorphism

  #138 opened 3 years ago by UlrikBuchholtz
  13

• Typo

  #137 opened 3 years ago by nicolaikraus
  1

• Epi-Mono decomposition for groups

  #136 opened 3 years ago by marcbezem
  2

• new notation for paths over

  #135 opened 3 years ago by DanGrayson
  7