Foundations based on ETCS

Question

So Id like to build a foundations based on ETCS. Here is what I found so far.

1. We define something called "category", using "domain" and "codomain" "functions". Yes, I know the properties, e.g. as they are defined in CWM. We also define functors and natural transformations in similar fasion.
2. We define ETCS as well-pointed (elementary) topos with NNO and choice, and accept the existence of this category. Originally it was defined a little bit different, but I use definition from nlab: ETCS.

Here is some questions.

1. What we really define as basis? E.g. for ZFC we know the existence of first order logic (not an expert in this topic).
2. What is the domain/codomain? Is it some form of predicate? If it is, how we define predicates (see question 1).
3. Can we use the existence/universal quantifiers? E.g. when we define terminal object (in definition of topos) we require a morphism to exist, and to be unique, meaning $Hom(X, T) = 1$.
4. How can we fully use the notion of $Hom$ set in generic category $C$? What I came up with: define a $Hom(X, Y)$ as a discrete category, whose objects are morphisms, and a set $H$ as discrete category $\{ 1 \to H\}$. Then category $C$ is locally small, iff there exists $H \in Set$ such that $H \cong Hom(X, Y)$ as categories. Note that we did not require all categories to be locally small as it is done in CWM.
5. What really means that we have equal morphisms? What I came up with: define morphism to be equal if diagram $X \rightrightarrows Y$ commutes. And define commuting diagram as done in nlab: commutative diagram. Problem is it uses posets or prosets, which both require the notion of unique morphism (we have a loop here).
6. I have a huge problem understanding well-pointiness axiom. Is it fine to say that: to define a function $X \to Y$ we need to define results on all elements, in other words, find morphism $1 \to X \to Y$ for all morphisms $1 \to X$. How can we formally deduce that $Hom(1, X) \cong X$ from existance of exp objects axiom? For now I only construct new functions as compositions of unique morphisms from universal constructions and "$id$"s.
7. Have a huge problem in understanding internal logic of sets and cocompleteness of ETCS. I only found this reference Todd Trimble on ETCS. What I want is formulate elementary colimts in terms of ETCS: initial object, coproducts, coequalizers, and ways to build new subsets: I know about correspondence between subobjects $A \hookrightarrow X$ and characteristic functions $\chi_A: X \to \Omega$, but what I really want is formalized ways to formulate something like an image: $$ f(A) := \{ y \in Y \mid \exists x \in A: f(x) = y \} \text{ for } A \hookrightarrow X,\ f: X \to Y. $$ Which building blocks did we used here to create a char-function? ETCS only implies existance of set $\{ x \in X \mid \phi(x) = true \} \subseteq X$.
8. Am I right that we can't get skeleton categories using set-choice? Is global choice fine? Set-choice imply Banach–Tarski paradox, does global choice even worse? As you see I really want skeletons, but it is fine if we can't.

Here is what I am looking for as an answer (any of these will be good):

1. Proper answers to my questions, using almost elementary theses. If you use something what is hard to find on the internet please add a reference. If it something easy, of course I know how to use wiki/nlab/some arxiv/math exchange etc.
2. Good books on these topics, as much as you can find. Id say, book is good if it doesn't use other books to much (unless it is highly needed), have something like common known facts in introduction, and have a respect to young readers, e.g. that don't know sheaves theory to much. Examples included. I guess these books are fairly easy to read, if you know what you are looking for. As far as I know, they don't cover my questions.

What I am not looking for.

1. Philosophical answers. I am not really interested in motivation or philosophical walk-arounds on notion of collections. All I want is good formalization.
2. Not interested in foundations based on ZFC (don't like it), Grothendieck universe (as done in CWM I guess), classes (they lead to notion of conglomerates) or other size walk-arounds. I really want a set to be defined as in ETCS, so it doesn't have elements and etc.

P.s.

1. Highly sorry for bad English. Not a native speaker (kind a joke phrase).
2. Highly sorry for disrespect to some areas of logic. Guess some youthful maximalism here.
3. As you see I done some research, and tried to introduce my own definitions. Still got stuck, mostly because of lack of experience and logic education.
4. Some questions are easy (but I still did not find an answer yet), while some require understanding resolution of size issues, that's quite hard I guess, so good reference will be good.
5. As a background, I am an algebra student (so I like formalizations) but not a logic expert (unfortunately). Knowing this will help understanding roots of my questions (I hope so).
6. Love Lawvere book, hope to find more like it. Is there modern intro notes on ETCC?
7. Feel free to post questions, edit this post (for admins I guess) and provide answers long time after question first appeared. I been thinking on this topic for almost a year, so I am patient enough.

MacLane, Saunders, Categories for the working mathematician., Graduate Texts in Mathematics, 5. New York etc.: Springer-Verlag. ix, 262 p. DM 58.00 (1988). ZBL0705.18001.

Lawvere, F. William, An elementary theory of the category of sets (long version) with commentary, Repr. Theory Appl. Categ. 2005, No. 11, 1-35 (2005). ZBL1072.18005.