Constructive Type Theory (CTT) is much closer in structure to informal mathematical thinking than, say, first-order predicate logic is. There are some examples of formalizing e.g. Euclidean proofs in CTT, but I'm struggling a little with the correct use of the syntax.
If we define a circle's circumference as a function type, ''a curve such that for a given point, all straight lines from that point to points on the curve are equal to some given length'', how would you you formulate this in type theory?
$$ circ(p,r):(\Pi p:Point)(\Pi r:Length)(\Sigma c: Curve)(\Pi x:StrL(p,c)) x\cong r $$
Is this correct? Is it fair to say that the function/proof-object $circ(\cdot,\cdot)$, applied to $a$ and $b$, is the circular line with center $a$ and radius $b$?