HoTT/Coq-HoTT

Issues

• Tensor product of cyclic groups

  #2022 opened 6 months ago by Alizter
  34

• grp_pow and related things

  #2015 opened 4 months ago by jdchristensen
  9

• Add break hints to =, ==, $==, $->

  #1927 opened 8 months ago by Alizter
  0

• Define free R-module as tensor product of R and free abelian group

  #2080 opened 4 months ago by Alizter
  0

• Fundamental theorem of arithmetic

  #2059 opened 4 months ago by Alizter
  1

• Prove that `n / (m / k) = (n * k) / m`

  #2073 opened 4 months ago by Alizter
  3

• Binomial Coefficients

  #2048 opened 4 months ago by Alizter
  0

• Add HasEquivs instance for MatrixCat

  #2046 opened 5 months ago by Alizter
  1

• Coq Platform and opam version lags

  #2045 opened 4 months ago by mikeshulman
  5

• Allow subgroups to be defined by predicates that don't take values in h-props

  #2069 opened 4 months ago by jdchristensen
  0

• Add functorality of cokernels and quotients for AbGroup

  #2067 opened 4 months ago by Alizter
  0

• use CongruenceQuotient to define coequalizer

  #2035 opened 4 months ago by jdchristensen
  9

• Prime numbers

  #2008 opened 4 months ago by Alizter
  0

• General Linear group

  #2006 opened 6 months ago by Alizter
  1

• Replace old definition of `cyclic` with new `cyclic'`

  #2051 opened 5 months ago by Alizter
  0

• Error: Unknown scope delimiting key _type.

  #2044 opened 5 months ago by ndcroos
  6

• Finite fields (Galois fields)

  #2007 opened 6 months ago by Alizter
  0

• Idempotent ring elements

  #2009 opened 6 months ago by Alizter
  0

• Define matrices as functions

  #1982 opened 7 months ago by Alizter
  2

• Define matrices as a collection of columns rather than a collection of rows

  #1983 opened 7 months ago by Alizter
  0

• Make pos and int unary

  #1913 opened 7 months ago by Alizter
  25

• Generalize lhs, lhs_V, rhs and rhs_V to all transitive relations

  #1950 opened 8 months ago by jdchristensen
  2

• Experiment with redefining bifunctors as uncurried functors

  #1933 opened 7 months ago by Alizter
  0

• Remove redundant fields from Ring

  #1945 opened 8 months ago by Alizter
  0

• Opposite ring

  #1921 opened 8 months ago by Alizter
  9

• Work out why test/WildCat/Opposite.v is slow

  #1936 opened 8 months ago by Alizter
  2

• dune frequently making full builds

  #1924 opened 8 months ago by jdchristensen
  9

• Spectral sequences

  #1932 opened 8 months ago by Alizter
  5

• Homological algebra lemmas

  #1931 opened 8 months ago by Alizter
  3

• Preservation of products

  #1889 opened 10 months ago by Alizter
  0

• Bifunctors

  #1883 opened 8 months ago by gio256
  13

• Tensor products of modules

  #1926 opened 8 months ago by Alizter
  0

• Add `_ $== _ :> _` notation exposing the underlying type of homs

  #1928 opened 8 months ago by Alizter
  0

• Use ViCaR to visualize terms in monoidal categories

  #1922 opened 8 months ago by Alizter
  3

• Add missing lemmas in PathGroupoids

  #1903 opened 8 months ago by Alizter
  0

• Show that pType has all coproducts

  #1890 opened 8 months ago by Alizter
  0

• Use `Attributes` command to deprecate usage of certain .v files

  #1904 opened 9 months ago by Alizter
  2

• Change definition of smash

  #1893 opened 9 months ago by Alizter
  2

• Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

  #1898 opened 9 months ago by rtetley
  5

• Project: coherence for monoidal categories

  #1896 opened 9 months ago by Alizter
  4

• Generalise results about wedge for pointed categories

  #1888 opened 10 months ago by Alizter
  0

• Dependences of Nat/Core.v and DProp.v

  #1882 opened 10 months ago by jdchristensen
  4

• HITs with rewrite rules

  #1868 opened 10 months ago by Alizter
  11

• slow builds with Coq 8.19 and/or dune 3.14.0

  #1866 opened 10 months ago by jdchristensen
  19

• Split HIT files into Core and lemmas

  #1855 opened 10 months ago by Alizter
  2

• Flattening lemma for GraphQuotient

  #1833 opened 10 months ago by Alizter
  6

• Add transport lemmas for families of equivalences

  #1841 opened 10 months ago by Alizter
  0

• coqdoc section links don't work for alectryon and timing toc pages

  #1775 opened a year ago by jdchristensen
  1

• Generalise ExactSequence.v to a pointed wildcat with kernels

  #1798 opened a year ago by Alizter
  1

• experiment with Hint Constants Opaque in typeclass search

  #1780 opened a year ago by jdchristensen
  3