Consider the following two kinds of transformation on proofs; the first is to make a a proof more incomplete, by erasing a lemma or a construction from it and replacing it by a tag saying this is obvious; the second kind of transformation takes a step that is proved by a this is obvious tag, applies some kind of prof-search algorithm to it, and replaces the tag by a real proof for that step. We will consider that the first operation goes toward the skeleton towards a more complete proof that had that skeleton as a projection. We are only interested in skeletons can be lifted back to full proofs using some known algorithm. In this thesis we can describe a language - DNC - that lets us prove several categorical facts using skeletons. The method for lifting these skeletons goes like this: from the name of a DNC term we can obtain its type; by a kind of Curry-Howard isomorphism a such type can be seen as a proposition in a certain logic; proof-search for that proposition will obtain a proof-tree for it in a certain system of Natural Deduction, and that proof-tree can be read as a lambda-term of given type - the proof-tree gives a natural construction for an object of the given type, that very often is exactly the object that we were looking for. Derivations in DNC can be translated into derivations in a Pure Type System with Dictionaries (PTSD), and derivations in PTSDs can be translated into derivations in Pure Type Systems (PTSs); so questions about the proof- theory of DNC become questions about the proof-theory of PTSs, whose properties are quite well-known. Also, not only we can lift names of terms in DNC to full proofs in different settings; for example, some proofs that apparently are happening over the category of sets can be reinterpreted as proofs over an arbitrary topos. We use that idea to give a simple presentation (in which the omitted obvious steps are obvious in a very precise sense) of the categorical semantics for some PTSs - and that includes PTSs into which the DNC derivations are translated.