# Tagged Questions

**15**

votes

**29**answers

725 views

### Formalizations of category theory in proof assistants

What are the existing formalizations of category theory in proof assistants?
I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, ...

**1**

vote

**2**answers

447 views

### How to interpret conflicting formal proofs about “a mod 0 = ? ”

The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.
According to Coq
$$ a \mod 0 = 0$$
and Isabelle proves
$$ a \mod = a$$
...

**2**

votes

**0**answers

854 views

### Why should I trust Coq when assumption-free proof of False in Coq exists? [closed]

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol).
Damien is critical of "fully certified decision procedure ...