funKanPowCounterModel-coq A Coq formalization of a countermodel to claim that the Kan property of simplicial sets are preserved under exponentiation constructively.