Proof Assistants Beta
Russoul's user avatar
Russoul's user avatar
Russoul's user avatar
Russoul
  • Member for 4 months
  • Last seen this week
Profile Activity
Stats
163
reputation
382
reached
0
answers
5
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
This user doesn’t have any silver badges yet.
5
bronze badges
Top tags
View all tags
0
Score
4
Posts
80
Posts %
0
Score
1
Posts
20
Posts %
0
Score
1
Posts
20
Posts %
0
Score
1
Posts
20
Posts %
0
Score
1
Posts
20
Posts %
0
Score
1
Posts
20
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
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
1
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
Apr 27
question
0
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?
2 hours ago

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.