Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer
  • Member for 14 years, 5 months
  • Last seen this week
7 votes

Is univalence equivalent to every type function being a functor over equivalence?

7 votes
Accepted

Uniqueness principle for functions types in the HoTT book

6 votes
Accepted

Type theory - category theory correspondence

6 votes

Monotonic and bounded sequences throughout mathematics

6 votes

Decidability theory involving real parameters

6 votes
Accepted

Construction of Dedekind reals using higher inductive-inductive types

6 votes

When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function defined on $[a, c]$?

6 votes
Accepted

Why isn't $S^1$ contractible in homotopy type theory?

6 votes
Accepted

Topos semantics of constructive higher order logic

6 votes

Why can't proofs have infinitely many steps?

6 votes

What logic is modelled by generalized boolean algebra?

6 votes

Is an ultrafinitist Hilbert's program doomed?

6 votes

The reals as continuous image of the irrationals

6 votes

A weaker concept of graph homomorphism

6 votes
Accepted

Why no morphisms from the contradictory proposition to the inconsistent context?

6 votes
Accepted

Is the category of quotient of countably based topological spaces cartesian closed ?

6 votes

Maximal ideal and Zorn's lemma

6 votes
Accepted

How many dimensions I need to embed a graph?

6 votes

Axiom of Infinity needed in Cantor-Bernstein?

6 votes

Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?

6 votes

"Internal" versus "external" definitions of functions: equivalent foundations for mathematics?

6 votes
Accepted

Analogy of $\omega$-models in constructive mathematics

6 votes

type theory that does not treat the terms of $\mathrm{Prop}$ as types

6 votes

What is $\sum_{i=0}^{n}\binom{n}{i}^3$?

6 votes
Accepted

Graphs with dangling edges

6 votes

Is a sentence true for two substructures also true for their intersection?

6 votes

Adding nonconstructive disjunction to intuitionistic logic

6 votes

Platonic Truth and 1st Order Predicate Logic

6 votes
Accepted

Inductive Definitions in Category Theory

6 votes

Noetherian Rings in Constructive Mathematics

1
6 7
8
9 10
12