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)))

PatrickMassot

/- The goal of this file is to explain why it's important that using extends in
   command `class foo extends bar` creates a `foo.to_bar` function with an 
   instance implicit parameter.
   
   We will define magmas with law denoted by ◆ and a commutative version.
   Then we want products of such things. The goal is to reuse the work on product
   magmas when defining product commutative magmas, and do so in a completely
   transparent way. -/

-- Defining magmas with some notation is already covered in TPIL