I don't see a reason why both viewpoints (and more) aren't accurate.
From one viewpoint, category theory provides a language for isolating abstract structures arising in a wide variety of areas of mathematics. The category theoretic notion of a 'product', for example, captures the notions of cartesian product of sets, direct sum of vector spaces, conjunction of formulae, greatest common divisor of integers, ...the list goes on. From this perspective, your first viewpoint applies (with more than just set theory, logic and type theory on top of the iceberg).
From another viewpoint, category theory is a setting for the semantics of different systems of logic: cartesian closed categories interpret $\lambda$-calculus, toposes interpret intuitionistic first-order logic, locally cartesian categories (kind of) interpret Martin-Löf dependent type theory, and so on. Categories have internal languages, which are type theories, and type theories have semantics in categories: this aligns more closely with your second picture.
From yet another viewpoint, a category is just a mathematical object built out of a couple of sets with some additional structure satisfying certain axioms, just like groups, rings, vector spaces, and so on. In this sense, category theory is just a branch of algebra which studies the algebraic properties of these algebraic structures that we call 'categories'. In this case, a more accurate picture would just be a small blob inside whatever foundational system you're working inside of.
So what is it? I don't think there is, or has to be, a single answer to your question.
(1) Yes. The particular dependent type theory one wants to use has UIP (Uniqueness of Identity Proofs), one universe of all propositions (in the homotopy-type-theory sense, i.e. subsingletons) satisfying propositional extensionality, pushouts (a kind of higher inductive type), and propositional truncations. This is a sort of truncated version of homotopy type theory.
(2) The type theory described above is one state of the art. Alternatively, one can use higher-order logic as described, for instance, in Sketches of an Elephant. I tend to prefer dependent type theory, since dependent types occur naturally in mathematics; but the semantics and metatheory are more difficult in that case (and filling in some of their details is a problem of current research).
(3) Agda, Coq, Idris can all manage this type theory easily, when suitably augmented by axioms (for UIP, propositional extensionality, etc.). The main wrinkle is that they all have a tower of universes, which an arbitrary elementary topos may not; but you can just ignore the larger universes. You can also reason in higher-order logic inside such a proof assistant by simply not making use of the dependent types.
Best Answer
The best introduction to category theory I know for non-mathematics students is Steve Awodey's Category Theory. Developed as an introduction to category theory for philosophy of mathematics students, the author has also used the original lecture notes to teach computer science majors as well. The book is careful,clear, has many examples and exercises and doesn't pour on too much hardcore mathematics. I consider it one of the best books out there for undergraduates on the subject and I think you might find it just what you're looking for.
I used to recommend Adowey all the time for undergraduates. But for mathematics students,to be honest, I'd prefer Harold Simmons' wonderful Introduction to Category Theory. It's beautifully written and pitched at about the same level as Awodey, but it's much more mathematical and contains far more algebra and topology then you might feel comfortable with. You might want to take a look at it, but be warned-it's really pitched at mathematics students.