Proof Assistants Beta
Russoul's user avatar
Russoul's user avatar
Russoul's user avatar
Russoul
  • Member for 11 months
  • Last seen more than a month ago
Profile Activity
Stats
345
reputation
917
reached
0
answers
7
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
This user doesn’t have any silver badges yet.
6
bronze badges
Top tags
View all tags
0
Score
7
Posts
100
Posts %
0
Score
2
Posts
29
Posts %
0
Score
2
Posts
29
Posts %
0
Score
1
Posts
14
Posts %
0
Score
1
Posts
14
Posts %
0
Score
1
Posts
14
Posts %
Top posts
All Questions Answers
Score Newest
question
9
What is the intuition behind the `Glue` type in Cubical Type Theories
Jan 3
question
4
Co-induction principle
Jun 13
question
3
State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types
May 20
question
2
Abstracting over large types in type theory
May 24
question
2
Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?
May 30
question
2
Provable `fun-ext`and "rewriting under binders" in intensional MLTT
Sep 2
question
1
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
Apr 27
Top network posts
View all network posts
7
Is is true that every monad transformer is equivalent to its underlying/base monad?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.