Ultimately I am trying to work my way towards defining an affine set in R^n. But to start I'm trying to work with points in QxQ with coefficients in Q. I want to define C a subset of QxQ as affine if for any x,y in C and t in Q, tx+(1-t)y is in C.
I read the answer to In Coq, how to define a set like A = {x | f(x) = 0}? which I think helped but I would need something more like C = { x | x = t1 * x1 + t2 * x2 where x1,x2 in C /\ t1 + t2 = 1}.
The difference between what you have and your linked question with A = {x | f(x) = 0} is that you aren't defining a single subset. Instead, you should define subsets in general then introduce a predicate to determine if a given subset is affine.
Let's start with what you want the definition to be.
I want to define C a subset of QxQ as affine if for any x,y in C and t in Q, tx+(1-t)y is in C.
So we should be given a subset C and say (informally still) IsAffine C := forall (x y: C) (t: Q), t * x + (1 - t) * y: C. This is pretty close to formal, though it uses some set theory conventions. The main one is that we don't prove that a given element is in a given type: the element has a fixed type whenever it's defined.
Really what we're saying here is that we have some notion of what it means for an element of R^n to be in the subset C. In fact, that's a perfectly good definition of subset: Subsets R^n := R^n -> Prop, that is, a subset is a function that takes a point and returns a proposition, which may or may not be true, depending on whether the point is in the subset. This is analogous to the powerset of a set X being 2^X in set theory, except we use Prop instead of 2.
Then to quantify over all the elements of a subset C: R^n -> Prop, we do something like forall x: R^n, C x -> ..., which could be read as "for all x in R^n, if x is in C, then ...".
So here's how I'd formalize what you want (given a definition of Q and definitions of scalar multiplication and vector addition).
Definition Subsets (A: Type) := A -> Prop.
Definition IsAffine (C: Subsets (Q * Q)) :=
forall (x y: Q * Q), C x -> C y -> forall t: Q, C (t * x + (1 - t) * y).