Stack Exchange

Dan Doel

Boston, MA, USA

top accounts reputation activity subscriptions
Top Questions
No questions with score of 5 or more
Top Answers
17
Is "all categorical reasoning formally contradictory"?
mathoverflow.net

15
Monad in Haskell programming vs. Monad in category theory
cs.stackexchange.com

13
What are well-founded inductive types?
proofassistants.stackexchange.com

13
What does canonicity property mean in Type Theory?
cs.stackexchange.com

13
Does this show that equality (set theoretically) does not necessarily imply isomorphic (categorically)?
math.stackexchange.com

10
Is Church-pentation implementable in Agda?
cstheory.stackexchange.com

10
Stronger "induction" principles than induction-recursion
cstheory.stackexchange.com

8
How do continuations represent negations (under the Curry–Howard correspondence)?
cstheory.stackexchange.com

8
Is induction over mutually inductive coinductive types possible?
proofassistants.stackexchange.com

8
Can you see that the Linz Halting Problem proof contains a fatal flaw?
cstheory.stackexchange.com

8
Glue types in cubical type theory
math.stackexchange.com

7
Are Rank2Types/RankNTypes practical without polytype variables?
stackoverflow.com

7
Reader, Writer monads
cstheory.stackexchange.com

7
Flawed argument in the proof of function extensionality in cubical type theory?
cs.stackexchange.com

7
What are some good (bad) examples of "green slime"?
proofassistants.stackexchange.com

7
How to prove that the Church encoding, forall r. (F r -> r) -> r, gives an initial algebra of the functor F?
cs.stackexchange.com

7
Curry-Howard isomorphism and non-constructive logic
cs.stackexchange.com

6
How does the elimination rule of the heterogeneous equality type imply a weak version of K?
proofassistants.stackexchange.com

6
Are Bad churches inhabited?
cs.stackexchange.com

6
Strictly-monotone "max" operation for constructive Brouwer-trees?
proofassistants.stackexchange.com

6
Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?
proofassistants.stackexchange.com

6
What are the implications of Homotopy Type Theory?
cs.stackexchange.com

5
Why does Agda's `--without-K` option also affect the indices of inductive types, where they have to be of lower levels?
proofassistants.stackexchange.com

5
Relationship between Higher Kinded Polymorphism, type inference, and Currying
cs.stackexchange.com

5
Stablishing termination of the construction of infinite stream with ranking functions
cs.stackexchange.com

5
How exactly do we define parametric polymorphism?
cs.stackexchange.com

5
What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
cs.stackexchange.com

5
Truncation and $\textsf{isProp}$
math.stackexchange.com

5
Why is the interval not a type but a pretype?
math.stackexchange.com

5
Motivation behind Lambda Calculus?
math.stackexchange.com

1 2