$lem:looping$. A homomorphism $F → G°$ is the same thing as a pair consisting of the set $L$ of edges of $F$ whose endpoints it identifies and a homomorphism $F ⊘ L → G$: the quotient by $L$ is exactly what remains once the collapsed edges are contracted, and an edge outside $L$ is sent to a genuine edge of $G$. Summing over $L$ gives the identity.