(If you're unfamiliar with the puzzles from To Mock a Mockingbird, three pages tell you everything you should need.)
Is it possible to solve the riddles in To Mock a Mockingbird in a "propositions as types" style?
As an example, let's take the second problem:
A bird x is called egocentric (sometimes narcissistic) if it is fond of itself—that is, if x's response to x is x. In symbols, x is egocentric if xx = x. The problem is to prove that under the given conditions $\text{C}_1$ and $\text{C}_2$ of the last problem, at least one bird is egocentric.
In something like Higher-Order Logic, I would define egocentricity like
definition egocentric :: "Bird => Bool" where
"egocentric A == (call A A = A)"
(assuming call :: Bird => Bird => Bird)
A naive attempt at encoding egocentricity as a type would be $$ \text{egocentric} : \textbf{Bird} \rightarrow \operatorname{call}(A,A)=A $$
However, an obvious problem is that $A$ isn't bound in the identity type
$$
\operatorname{call}(A,A)=A
$$
(which, in HoTT is "judgmentally equal" to the type $\textbf{Id}_{\textbf{Bird}}(\operatorname{call}(A,A), A)$)
So, we need a dependent function definition, right?
$$
\text{egocentric} : \Pi A:\textbf{Bird}. call(A, A) =_\textbf{Bird} A
$$
But... that doesn't look like the type-theory equivalent of an unary predicate; it looks like the claim "Every bird's response to its own name is its name"!
If it's helpful to instead ask a very specific question:
Given the "composition" and "mockingbird" conditions (q.v. the book's first exercise), how would you construct a term of the following type? $$\Pi A:\textbf{Bird}. \Sigma x:\textbf{Bird}. \operatorname{call}(A, x) = x$$ (Sorta implicit: how would you encode the "composition" and "mockingbird" givens?)
Let's take things slowly. First things first: $\mathsf{egocentric}$ is a predicate, so it is a $\mathsf{Type}$-valued function of some kind. In this case, it is a function $\mathsf{Bird} \to \mathsf{Type}$. It is defined as follows: $$\mathsf{egocentric} \equiv \lambda A : \mathsf{Bird} . \mathsf{call}(A, A) =_{\mathsf{Bird}} A$$ Thus: $$\mathop{\mathsf{egocentric}} A \equiv \mathsf{call}(A, A) =_{\mathsf{Bird}} A$$
That said, I question your motives. There is no benefit in thinking about the problem in this way. It is more useful to work directly with the (typed) $\lambda$-calculus built into type theory than to build try an internal model of it.