With recent developments in homotopy type theory, we can prove and mechanize type-theoretic versions of homotopy-theoretic theorems, which leads to "synthetic homotopy theory". In this talk I will focus on the Seifert–van Kampen theorem, which relates the loop structure of a space obtained by gluing to the loop structures of individual components. This theorem is useful because gluing is widespread in topology, and loop structures help distinguish spaces. I will discuss about the proof and the mechanization in the proof assistant Agda.