Module two_type 

A genuinely 2-truncated ∞-groupoid, had as an object: the minimal K(A, 2).

kan_complex built the nerve BG = K(G, 1) and proved it 1-truncated (inner horns fill uniquely). This is the first object beyond that — a Kan complex with real π₂ ≠ 0 living inside it, not merely admitted by a crossed module or glimpsed as homology. It is the Eilenberg–MacLane space K(A, 2): π₂ = A, every other πₙ = 0.

The model is Dold–Kan Γ(A[2]) for the chain complex with A in degree 2. Its n-simplices are the A-linear combinations of order-preserving surjections [n] ↠ [2] (since the complex is concentrated in degree 2, a face that fails to stay surjective dies — C₁ = C₃ = 0). Concretely an n-simplex is an A-labeling of S_n = {surjections [n] ↠ [2]}, and dᵢ pulls back along the i-th coface, keeping only the still-surjective terms. It is a simplicial abelian group, hence automatically a Kan complex — and we verify, by enumeration:

• π₂ ≠ 0: the inner horn Λ²₁ has |A| fillers (the 2-cells), not the unique filler of a 1-type. This is the structure K(G,1) provably lacked.
• Kan: every horn fills (the face-tuple map onto the compatible-horn object is surjective), checked in degrees 2, 3, 4.
• exactly 2-truncated: degree-4 inner horns fill uniquely again (no π₃), so the higher homotopy stops at level 2.