/lean-groupoids

first-order groupoids and tactics for the Lean Theorem Prover

Primary LanguageLeanApache License 2.0Apache-2.0

Lean Groupoids

A first-order implementation of groupoids for Lean. Includes tactics for working with setoids, including equality.