proposition: Lemma one_point_theory_algebra_is_trivial : ∏ (A : algebra one_point_theory), A ≃ unit.
proof: Proof. intro A. apply weqcontrtounit. use tpair. - use (action (tt : (one_point_theory 0 : hSet)) (weqvecfun 0 vnil)). - intro a. rewrite <- (pr_action _ (make_stn 1 0 (idpath _)) (λ _, a) : _ = a). exact (lift_constant_action _ _ _). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Functors UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.Algebras