[ukj]

A-priori truths are called axioms.

In the context of the Curry-Howard isomorphism you don't "prove things about programs".

Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language like Agda, Coq or Idris.

The link in my post to the UniMath project is a bunch of codified proofs to various theorems in Category theory, Topology, Combinatorics etc.

[howardcurry]

I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth.

Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.

[joycian]

If it has been proven from your axioms (really down from the axioms!) then you can add it to a library of statements you 'know' (or in the case of your axioms, assume) to be true.

[ukj]

More succinctly: The thing you want proven is a proposition.

A proposition is a type. Writing the algorithm which implements the type is the same as proving it.

https://ncatlab.org/nlab/show/propositions+as+types

[ukj]

A theorem is a consequence of a set of axioms. By definition.

It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom.

Wanting to prove that X is a theorem of a-priori truth Y is the same thing as writing the algorithm for f: Y -> X