PatrickMassot

import algebra.ring
import group_theory.submonoid
import tactic.interactive

namespace tactic

open tactic.interactive

meta def derive_field_subtype : tactic unit :=
do b ← target >>= is_prop,

PatrickMassot

import order.basic .simplex_category data.finset data.finsupp algebra.group

local notation ` [`n`] ` := fin (n+1)

/-- Simplicial set -/
class simplicial_set :=
(objs : Π n : ℕ, Type*)
(maps {m n : ℕ} {f : [m] → [n]} (hf : monotone f) : objs n → objs m)
(comp {l m n : ℕ} {f : [l] → [m]} {g : [m] → [n]} (hf : monotone f) (hg : monotone g) :
  (maps hf) ∘ (maps hg) = (maps (monotone_comp hf hg)))