Skip to main content
Proof Assistants Beta
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel
  • Member for 2 years, 7 months
  • Last seen this week
  • Boston, MA, USA
Profile Activity
Stats
982
reputation
4k
reached
14
answers
0
questions
Communities
View all
Badges
View all badges
This user doesn’t have any gold badges yet.
5
silver badges
7
bronze badges
Top tags
View all tags
22
Score
2
Posts
14
Posts %
15
Score
3
Posts
21
Posts %
14
Score
2
Posts
14
Posts %
13
Score
3
Posts
21
Posts %
11
Score
2
Posts
14
Posts %
10
Score
2
Posts
14
Posts %
Top posts
View all questions and answers
answer
14
What are well-founded inductive types?
Mar 2, 2022
answer
8
Is induction over mutually inductive coinductive types possible?
Mar 6, 2022
answer
7
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
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
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"?
15
Monad in Haskell programming vs. Monad in category theory
13
Does this show that equality (set theoretically) does not necessarily imply isomorphic (categorically)?
13
What does canonicity property mean in Type Theory?
11
Stronger "induction" principles than induction-recursion