UniMath/agda-unimath issues and pull requests

#1010 - Fix "The predicate of" section headers

Pull Request - State: open - Opened by EgbertRijke 10 months ago

#1010 - Fix "The predicate of" section headers

Pull Request - State: open - Opened by EgbertRijke 10 months ago

#1009 - Equivalence injective type families

Pull Request - State: open - Opened by fredrik-bakke 10 months ago - 2 comments
Labels: foundation

#1009 - Equivalence injective type families

Pull Request - State: open - Opened by fredrik-bakke 10 months ago - 2 comments
Labels: foundation

#1008 - Add operators of the form `Prop → Prop`

Pull Request - State: open - Opened by fredrik-bakke 10 months ago - 2 comments
Labels: question, foundation, refactoring

#1007 - Span diagrams

Pull Request - State: open - Opened by EgbertRijke 10 months ago - 3 comments
Labels: foundation

#1007 - Span diagrams

Pull Request - State: open - Opened by EgbertRijke 10 months ago - 3 comments
Labels: foundation

#1006 - Fix link name for the Formatting section of the codestyle

Pull Request - State: closed - Opened by VojtechStep 10 months ago - 1 comment

#1005 - Basic properties of the flat modality

Pull Request - State: open - Opened by fredrik-bakke 10 months ago
Labels: modal-type-theory

#1004 - Reformatting commented blocks of code

Pull Request - State: closed - Opened by EgbertRijke 10 months ago - 1 comment
Labels: formatting

#1003 - Hatcher's acyclic type is acyclic

Pull Request - State: closed - Opened by tomdjong 10 months ago - 2 comments
Labels: synthetic-homotopy-theory

#1002 - Render ASCII diagrams as SVGs using svgbob

Pull Request - State: closed - Opened by fredrik-bakke 10 months ago - 15 comments
Labels: website, tooling, do not merge

#1001 - Lifts of types

Pull Request - State: closed - Opened by EgbertRijke 10 months ago - 5 comments
Labels: foundation

#1000 - Universal property of contractible types w.r.t. pointed types and maps

Pull Request - State: closed - Opened by tomdjong 10 months ago - 5 comments
Labels: structured-types

#999 - Extensions of types

Pull Request - State: closed - Opened by EgbertRijke 10 months ago - 12 comments
Labels: foundation

#998 - Make type arguments implicit for `eq-equiv`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 4 comments
Labels: refactoring

#997 - Rename `is-prop-Π'` to `is-prop-implicit-Π` and `Π-Prop'` to `implicit-Π-Prop`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 1 comment
Labels: refactoring

#996 - Rename `3-simplex` to `tetrahedron`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago
Labels: foundation, refactoring

#995 - Make type family implicit for `is-torsorial-Eq-structure` and `is-torsorial-Eq-Π`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 2 comments
Labels: refactoring

#994 - Use `point x` instead of `const unit X x`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 4 comments
Labels: refactoring

#993 - Make type argument explicit for `terminal-map`

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 2 comments
Labels: refactoring

#992 - Resolve duplicate definitions

Issue - State: open - Opened by VojtechStep 11 months ago
Labels: help wanted, cleanup

#991 - Deduplicate singleton-induction

Pull Request - State: closed - Opened by VojtechStep 11 months ago - 3 comments
Labels: repo-maintenance

#990 - Rename "towers" to "inverse sequential diagrams"

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 3 comments
Labels: foundation, refactoring

#989 - Exponentiating retracts of maps

Pull Request - State: closed - Opened by fredrik-bakke 11 months ago - 8 comments
Labels: foundation, orthogonal-factorization-systems

#988 - Refactor properties of lifts of families out of 26-descent

Pull Request - State: open - Opened by VojtechStep 11 months ago - 9 comments

#987 - Respect agda flags set in the Makefile during CI builds

Pull Request - State: closed - Opened by VojtechStep 11 months ago - 2 comments
Labels: bug, CI

#986 - Bump Agda max heap limit

Pull Request - State: closed - Opened by VojtechStep 11 months ago
Labels: CI, fix

#985 - Investigate memory usage when typechecking the whole library

Issue - State: open - Opened by VojtechStep 11 months ago
Labels: help wanted, CI

#984 - Competing conventions for operations on propositions

Issue - State: open - Opened by fredrik-bakke 12 months ago - 5 comments

#983 - Some minor refactoring surrounding Dedekind reals

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 5 comments
Labels: foundation, real-numbers, refactoring

#982 - Discuss replacing `-whisk-` with `-whisker-`

Issue - State: open - Opened by VojtechStep 12 months ago - 1 comment

#981 - Swap order of arguments for lifts of families of elements

Pull Request - State: closed - Opened by VojtechStep 12 months ago - 1 comment
Labels: orthogonal-factorization-systems, refactoring

#980 - Fix urls

Pull Request - State: closed - Opened by tomdjong 12 months ago

#979 - Basic properties of orthogonal maps

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 12 comments
Labels: foundation, orthogonal-factorization-systems

#978 - Refactor functoriality and various infrastructure for sequential colimits

Pull Request - State: closed - Opened by VojtechStep 12 months ago - 6 comments
Labels: synthetic-homotopy-theory, refactoring

#977 - small addendum to copartial elements, and proposal of erased -> denied

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 1 comment
Labels: foundation

#976 - Improve generality of homotopy whiskering operations

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 11 comments
Labels: foundation

#975 - Partial and copartial functions

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 7 comments
Labels: foundation

#974 - Precomposition retracts of maps

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 12 comments
Labels: foundation, orthogonal-factorization-systems

#973 - Action on homotopies of functions

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 5 comments
Labels: foundation, refactoring

#972 - Flattening lemma for sequential colimits

Pull Request - State: closed - Opened by VojtechStep 12 months ago - 7 comments
Labels: synthetic-homotopy-theory

#971 - Typos in the universal property of the family of fibers of a map

Pull Request - State: closed - Opened by EgbertRijke 12 months ago
Labels: typo

#970 - The Hardy-Ramanujan number

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 2 comments
Labels: elementary-number-theory

#969 - The `is-sequential-colimit` predicate

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 1 comment
Labels: synthetic-homotopy-theory

#968 - Retracts of sequential diagrams induce retracts of sequential colimits

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 1 comment
Labels: synthetic-homotopy-theory

#967 - `k`-acyclic maps/types closure properties

Pull Request - State: closed - Opened by tomdjong 12 months ago - 2 comments
Labels: foundation, synthetic-homotopy-theory

#966 - Add `is-sequential-colimit`

Issue - State: closed - Opened by VojtechStep 12 months ago
Labels: synthetic-homotopy-theory

#965 - Sync up nomenclature between towers and cotowers

Issue - State: closed - Opened by VojtechStep 12 months ago - 3 comments
Labels: foundation, synthetic-homotopy-theory

#964 - Retracts of sequential diagrams

Issue - State: closed - Opened by VojtechStep 12 months ago - 1 comment
Labels: help wanted, synthetic-homotopy-theory

#963 - Refactor universal properties for various limits

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 1 comment
Labels: foundation, refactoring

#962 - Update reflection for 2.6.4

Pull Request - State: closed - Opened by FernandoChu 12 months ago
Labels: reflection

#961 - Refactor universal property of suspensions

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 10 comments
Labels: synthetic-homotopy-theory, refactoring

#960 - Closure properties of acyclic maps and types

Pull Request - State: closed - Opened by tomdjong 12 months ago - 1 comment
Labels: synthetic-homotopy-theory

#959 - Play with `hom-arrow` as a record

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 4 comments
Labels: question, refactoring, do not merge

#958 - Torsoriality of multivariable homotopies

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 2 comments
Labels: foundation, refactoring

#957 - Bibliography

Issue - State: open - Opened by EgbertRijke 12 months ago - 1 comment
Labels: enhancement

#956 - A type is `1`-acyclic if and only if it is `0`-connected

Pull Request - State: closed - Opened by tomdjong 12 months ago - 7 comments
Labels: synthetic-homotopy-theory

#955 - Adding more tags

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 6 comments
Labels: repo-maintenance

#954 - Characterization of acyclic types in terms of `const` to identity types being an equivalence

Pull Request - State: closed - Opened by tomdjong 12 months ago
Labels: foundation, synthetic-homotopy-theory

#953 - Adding more concept tags to graph theory

Pull Request - State: closed - Opened by EgbertRijke 12 months ago
Labels: repo-maintenance

#952 - Adding concept tags to three files

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 1 comment
Labels: repo-maintenance

#951 - Suspensions increase connectedness and relating `k`-acyclic maps, `k`-equivalences and `k`-connected maps

Pull Request - State: closed - Opened by tomdjong 12 months ago - 1 comment
Labels: synthetic-homotopy-theory

#950 - Comment on the name `is-truncated-acyclic`

Pull Request - State: closed - Opened by tomdjong 12 months ago
Labels: synthetic-homotopy-theory

#949 - A map is `k`-acyclic iff it is a `k`-epi iff it is a dependent `k`-epi

Pull Request - State: closed - Opened by tomdjong 12 months ago
Labels: foundation, synthetic-homotopy-theory

#948 - `k`-acyclic types

Pull Request - State: closed - Opened by tomdjong 12 months ago - 1 comment
Labels: foundation, synthetic-homotopy-theory

#947 - Define (sequentially) compact types

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 1 comment
Labels: foundation, synthetic-homotopy-theory

#946 - Idea: use coherently invertible maps as default notion of equivalence

Issue - State: open - Opened by fredrik-bakke 12 months ago
Labels: enhancement, help wanted, question, foundation, refactoring

#945 - Refactor categories to carry a bidirectional witness of associativity

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago
Labels: category-theory, refactoring

#944 - Universal property of fibers

Pull Request - State: closed - Opened by morphismz 12 months ago - 4 comments
Labels: foundation

#943 - Reverse the direction of the equivalences on hom-sets in adjunctions

Pull Request - State: closed - Opened by EgbertRijke 12 months ago - 4 comments
Labels: category-theory

#942 - Update maintainer sentences

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago
Labels: documentation

#941 - Subterminal precategories and constant functors

Pull Request - State: closed - Opened by fredrik-bakke 12 months ago - 1 comment
Labels: category-theory

#940 - A map is `k`-epic iff its codiagonal is `k`-connected iff its codiagonal is a `k`-equivalence

Pull Request - State: closed - Opened by tomdjong 12 months ago - 2 comments
Labels: foundation

#939 - Autoformatting for Python files

Issue - State: open - Opened by fredrik-bakke 12 months ago - 3 comments
Labels: CI, pre-commit

#938 - Necessary truncations on formalizing cardinal arithmetic

Issue - State: open - Opened by ElifUskuplu 12 months ago
Labels: set-theory

#937 - Refactor precomposition

Pull Request - State: closed - Opened by EgbertRijke almost 1 year ago - 5 comments
Labels: foundation, refactoring

#936 - Several facts about `k`-equivalences

Pull Request - State: closed - Opened by tomdjong almost 1 year ago - 1 comment
Labels: foundation

#935 - The orbit category of a group

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 3 comments
Labels: group-theory, category-theory

#934 - Idea: refactor (nonunital) precategories to have both directions of the associativity witness

Issue - State: closed - Opened by fredrik-bakke about 1 year ago - 1 comment
Labels: enhancement, category-theory, refactoring

#933 - Idea: refactor categories to build on the theory of wild categories

Issue - State: open - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: help wanted, category-theory, structured-types, refactoring

#932 - Refactor categories to come equipped with an identity system on its morphisms

Issue - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: category-theory, refactoring

#931 - Initial definitions for the cd-excision project

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: foundation, orthogonal-factorization-systems

#930 - Project: Sheaves and excision with respect to regular cd-structures

Issue - State: open - Opened by EgbertRijke about 1 year ago - 1 comment
Labels: synthetic-homotopy-theory, orthogonal-factorization-systems

#929 - Optimize proof of `equiv-natural-isomorphism-htpy-map-is-category-Precategory`

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 2 comments
Labels: category-theory

#928 - Fix some typos in the mixfix guide

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: fix, guides

#927 - Pushout-products, fiberwise joins, and dependent pushout-products

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 2 comments
Labels: synthetic-homotopy-theory

#926 - The equivalences on hom-sets in adjunctions of large (pre)categories go the unnatural way

Issue - State: closed - Opened by EgbertRijke about 1 year ago - 1 comment
Labels: category-theory, refactoring

#925 - Identity system on implicit Pi types

Issue - State: closed - Opened by EgbertRijke about 1 year ago - 4 comments
Labels: foundation

#924 - Infrastructure for homotopies between maps out of a suspension

Pull Request - State: closed - Opened by morphismz about 1 year ago - 5 comments
Labels: foundation, synthetic-homotopy-theory

#923 - Cellular maps

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago
Labels: orthogonal-factorization-systems

#922 - Displayed precategories

Pull Request - State: open - Opened by fredrik-bakke about 1 year ago
Labels: category-theory

#921 - The class of `k`-epis is closed under composition and has the right cancellation property

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: foundation

#920 - Codingstyle guideline that definitions should be specified

Pull Request - State: closed - Opened by EgbertRijke about 1 year ago - 7 comments
Labels: category-theory, guides

#919 - Functoriality of sequential colimits

Pull Request - State: closed - Opened by VojtechStep about 1 year ago - 14 comments
Labels: foundation, synthetic-homotopy-theory

#918 - A map is a `k`-epi iff its codiagonal is a `k`-equivalence

Pull Request - State: closed - Opened by tomdjong about 1 year ago - 3 comments
Labels: foundation

#917 - Change the universal property of epimorphisms, so that it is stated with respect to all universe levels

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: foundation

#916 - If `f` is a `k`-epi, then so is its `k`-truncation

Pull Request - State: closed - Opened by tomdjong about 1 year ago
Labels: foundation

#915 - Miscellaneous Agda configuration maintenance

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago
Labels: repo-maintenance

#914 - Cubical compatibility

Pull Request - State: closed - Opened by fredrik-bakke about 1 year ago - 22 comments
Labels: repo-maintenance

GitHub / UniMath/agda-unimath issues and pull requests