MathOverflow
András Kovács's user avatar
András Kovács's user avatar
András Kovács's user avatar
András Kovács
  • Member for 10 years, 8 months
  • Last seen more than a month ago
Profile Activity
Stats
199
reputation
1k
reached
2
answers
0
questions
Communities
View all
About

Type theory researcher at ELTE Budapest.

Badges
This user doesn’t have any gold badges yet.
This user doesn’t have any silver badges yet.
8
bronze badges
Top tags
10
Score
2
Posts
100
Posts %
8
Score
1
Posts
50
Posts %
8
Score
1
Posts
50
Posts %
Top posts
answer
8
Is $\prod_{X : \mathcal{U}} (X \to X) \cong 1$ consistent with type theory?
Feb 21, 2020
answer
2
Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?
Jan 10, 2022
Top network posts
View all network posts
104
Erratic hole type resolution
66
Haskell program involving `read` is much slower than an equivalent Python one
33
Doing rank-n quantification in Idris
31
Compatibility of impredicative Set and function extensionality
27
Online reference book for *implementing* concepts in type theory.