Proof Assistants Beta
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel
  • Member for 1 year, 3 months
  • Last seen this week
  • Boston, MA, USA
Profile Activity
Stats
930
reputation
3k
reached
13
answers
0
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
4
silver badges
6
bronze badges
Top tags
View all tags
21
Score
2
Posts
15
Posts %
15
Score
3
Posts
23
Posts %
14
Score
2
Posts
15
Posts %
13
Score
1
Posts
8
Posts %
11
Score
2
Posts
15
Posts %
10
Score
2
Posts
15
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
13
What are well-founded inductive types?
Mar 2, 2022
answer
8
Is induction over mutually inductive coinductive types possible?
Mar 6, 2022
answer
6
Strictly-monotone "max" operation for constructive Brouwer-trees?
Jun 3, 2022
answer
6
How does the elimination rule of the heterogeneous equality type imply a weak version of K?
Feb 12, 2022
answer
6
What are some good (bad) examples of "green slime"?
Jul 23, 2022
answer
6
Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?
Sep 15, 2022
answer
5
Why does Agda's `--without-K` option also affect the indices of inductive types, where they have to be of lower levels?
Feb 12, 2022
answer
4
Is there any universe polymorphic version of univalence?
Feb 24, 2022
answer
4
Can I use if_then_else on indexed paths in HITs?
Mar 1, 2022
answer
4
Counting in two ways
Jun 17, 2022
Top network posts
View all network posts
17
Is "all categorical reasoning formally contradictory"?
14
Monad in Haskell programming vs. Monad in category theory
13
Does this show that equality (set theoretically) does not necessarily imply isomorphic (categorically)?
12
What does canonicity property mean in Type Theory?
10
Is Church-pentation implementable in Agda?

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.