Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Mathlib.CategoryTheory.FinCat.Hom2Decidable equality of specifications
Equality is decidable at each of the three levels: finite-category
specifications, functor specifications and 2-cell specifications. Each
level is decided field by field, transporting along the equality of an
earlier field wherever a later field's type mentions it. The Bool
equation fields are proof-irrelevant and contribute no decision.
Main definitions
CategoryTheory.FinCat.decidableEqPiFin — equality of functions out
of Fin n, decided pointwise.
CategoryTheory.FinCat.decidableEqComp — equality of composition
tables at fixed counts.
CategoryTheory.FinCat.Hom₂.decidableEq,
CategoryTheory.FinCat.Hom.decidableEq,
CategoryTheory.FinCat.decidableEq — the three levels.
Implementation notes
decidableEqPiFin is dependent from the outset, funext_iff already
being so, and therefore covers the non-dependent case with no second
instance at the same head symbol.
It is scoped, and every DecidableEq argument at a Π-type use site
is supplied explicitly, one application per binder, so that the only
argument left to instance resolution is the innermost
DecidableEq (Fin _), where core's instance is the sole candidate.
Fintype.decidablePiFintype is a competitor at the same head symbol
and is likewise dependent, so the two measures are needed together:
without the scoping, which of the two applies downstream would be a
matter of declaration order, and without the explicit arguments the
inner ones resolve through it.
The transports run in the order the fields are declared. At the
specification level objCount is a Nat, decided by core's
Nat.decEq through a dif, and nonIdCount and comp follow; at
the functor level objMap precedes map, whose type mentions it; at
the 2-cell level app's type mentions only the fixed 1-cells F and
G, so no transport arises.
Beyond its own dependency this module needs no import: funext_iff
and decidable_of_iff are core.
Tags
category, functor, natural transformation, finite category, decidable equality, constructive, choice-free
@[expose] public sectionnamespace CategoryTheorynamespace FinCat
Decidable equality of functions out of Fin n, decided pointwise.
Dependent from the outset — funext_iff already is — so it covers the
non-dependent case with no second instance at the same head symbol.
scoped instance decidableEqPiFin.{v} {n : Nat} {Y : Fin n → Type v}
[∀ i, DecidableEq (Y i)] : DecidableEq ((i : Fin n) → Y i) :=
fun f g ↦ decidable_of_iff (∀ i, f i = g i) funext_iff.symm
Decidable equality of composition tables at fixed counts. The
DecidableEq argument is supplied explicitly at every level: an
instance that still typechecks may silently acquire
Classical.choice, which is the hazard Geb/Mathlib/Data/FinEnum.lean
documents for the same head symbol.
def decidableEqComp {objCount : Nat} {nonIdCount : Fin objCount → Fin objCount → Nat} :
DecidableEq ((i j k : Fin objCount) → Fin (nonIdCount i j) → Fin (nonIdCount j k) →
Fin (homCountOf objCount nonIdCount i k)) :=
@decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦ inferInstance)))))
Decidable equality of 2-cell specifications. No transport: app's
type mentions only the fixed parameters F and G.
instance Hom₂.decidableEq {S T : FinCat} {F G : Hom S T} :
DecidableEq (Hom₂ F G) :=
fun α β ↦
match α, β with
| ⟨a, _⟩, ⟨b, _⟩ =>
match @decidableEqPiFin _ _ (fun _ ↦ inferInstance) a b with
| isTrue h => isTrue (S:FinCatT:FinCatF:S.Hom TG:S.Hom Tα:Hom₂ F Gβ:Hom₂ F Ga:(i : Fin S.objCount) → T.Mor (F.objMap i) (G.objMap i)natValid✝¹:natCheckOf S T F G a = trueb:(i : Fin S.objCount) → T.Mor (F.objMap i) (G.objMap i)natValid✝:natCheckOf S T F G b = trueh:a = b⊢ { app := a, natValid := natValid✝¹ } = { app := b, natValid := natValid✝ } S:FinCatT:FinCatF:S.Hom TG:S.Hom Tα:Hom₂ F Gβ:Hom₂ F Ga:(i : Fin S.objCount) → T.Mor (F.objMap i) (G.objMap i)natValid✝¹:natCheckOf S T F G a = truenatValid✝:natCheckOf S T F G a = true⊢ { app := a, natValid := natValid✝¹ } = { app := a, natValid := natValid✝ }; All goals completed! 🐙)
| isFalse h => isFalse (fun e ↦ h (S:FinCatT:FinCatF:S.Hom TG:S.Hom Tα:Hom₂ F Gβ:Hom₂ F Ga:(i : Fin S.objCount) → T.Mor (F.objMap i) (G.objMap i)natValid✝¹:natCheckOf S T F G a = trueb:(i : Fin S.objCount) → T.Mor (F.objMap i) (G.objMap i)natValid✝:natCheckOf S T F G b = trueh:¬a = be:{ app := a, natValid := natValid✝¹ } = { app := b, natValid := natValid✝ }⊢ a = b All goals completed! 🐙))
Decidable equality of functor specifications: decide objMap,
transport along that equality — map's type mentions objMap — then
decide map.
instance Hom.decidableEq {S T : FinCat} : DecidableEq (Hom S T) :=
fun F G ↦
match F, G with
| ⟨o, m, _⟩, ⟨o', m', _⟩ =>
match @decidableEqPiFin _ _ (fun _ ↦ inferInstance) o o' with
| isFalse h => isFalse (fun e ↦ h (S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = trueo':Fin S.objCount → Fin T.objCountm':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o' i) (o' j)compValid✝:compCheckOf S T o' m' = trueh:¬o = o'e:{ objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o', map := m', compValid := compValid✝ }⊢ o = o' All goals completed! 🐙))
S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = trueo':Fin S.objCount → Fin T.objCountm':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o' i) (o' j)compValid✝:compCheckOf S T o' m' = trueho:o = o'⊢ Decidable ({ objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o', map := m', compValid := compValid✝ }) S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = trueo':Fin S.objCount → Fin T.objCountm':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o' i) (o' j)compValid✝:compCheckOf S T o' m' = trueho:o = o'⊢ Decidable ({ objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o', map := m', compValid := compValid✝ })
S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = truem':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝:compCheckOf S T o m' = true⊢ Decidable ({ objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o, map := m', compValid := compValid✝ })
exact match @decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦ inferInstance))) m m' with
| isTrue h => isTrue (S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = truem':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝:compCheckOf S T o m' = trueh:m = m'⊢ { objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o, map := m', compValid := compValid✝ } S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = truecompValid✝:compCheckOf S T o m = true⊢ { objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o, map := m, compValid := compValid✝ }; All goals completed! 🐙)
| isFalse h => isFalse (fun e ↦ h (S:FinCatT:FinCatF:S.Hom TG:S.Hom To:Fin S.objCount → Fin T.objCountm:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝¹:compCheckOf S T o m = truem':(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (o i) (o j)compValid✝:compCheckOf S T o m' = trueh:¬m = m'e:{ objMap := o, map := m, compValid := compValid✝¹ } = { objMap := o, map := m', compValid := compValid✝ }⊢ m = m' All goals completed! 🐙))
Decidable equality of specifications: decide objCount, transport,
decide nonIdCount, transport, decide comp.
instance decidableEq : DecidableEq FinCat := fun S T ↦
match S, T with
| ⟨n, nc, c, _⟩, ⟨n', nc', c', _⟩ =>
if hn : n = n' then S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truen':ℕnc':Fin n' → Fin n' → ℕc':(i j k : Fin n') → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n' nc' i k)assoc✝:assocCheckOf n' nc' c' = truehn:n = n'⊢ Decidable
({ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n', nonIdCount := nc', comp := c', assoc := assoc✝ })
S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truenc':Fin n → Fin n → ℕc':(i j k : Fin n) → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n nc' i k)assoc✝:assocCheckOf n nc' c' = true⊢ Decidable
({ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc', comp := c', assoc := assoc✝ })
exact match @decidableEqPiFin _ _ (fun _ ↦
@decidableEqPiFin _ _ (fun _ ↦ inferInstance)) nc nc' with
| isFalse h => isFalse (fun e ↦ h (S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truenc':Fin n → Fin n → ℕc':(i j k : Fin n) → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n nc' i k)assoc✝:assocCheckOf n nc' c' = trueh:¬nc = nc'e:{ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc', comp := c', assoc := assoc✝ }⊢ nc = nc' All goals completed! 🐙))
S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truenc':Fin n → Fin n → ℕc':(i j k : Fin n) → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n nc' i k)assoc✝:assocCheckOf n nc' c' = truehnc:nc = nc'⊢ Decidable
({ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc', comp := c', assoc := assoc✝ }) S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truenc':Fin n → Fin n → ℕc':(i j k : Fin n) → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n nc' i k)assoc✝:assocCheckOf n nc' c' = truehnc:nc = nc'⊢ Decidable
({ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc', comp := c', assoc := assoc✝ })
S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truec':(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝:assocCheckOf n nc c' = true⊢ Decidable
({ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc, comp := c', assoc := assoc✝ })
exact match decidableEqComp c c' with
| isTrue h => isTrue (S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truec':(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝:assocCheckOf n nc c' = trueh:c = c'⊢ { objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc, comp := c', assoc := assoc✝ } S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = trueassoc✝:assocCheckOf n nc c = true⊢ { objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝ }; All goals completed! 🐙)
| isFalse h => isFalse (fun e ↦ h (S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truec':(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝:assocCheckOf n nc c' = trueh:¬c = c'e:{ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n, nonIdCount := nc, comp := c', assoc := assoc✝ }⊢ c = c' All goals completed! 🐙))
else isFalse (fun e ↦ hn (S:FinCatT:FinCatn:ℕnc:Fin n → Fin n → ℕc:(i j k : Fin n) → Fin (nc i j) → Fin (nc j k) → Fin (homCountOf n nc i k)assoc✝¹:assocCheckOf n nc c = truen':ℕnc':Fin n' → Fin n' → ℕc':(i j k : Fin n') → Fin (nc' i j) → Fin (nc' j k) → Fin (homCountOf n' nc' i k)assoc✝:assocCheckOf n' nc' c' = truehn:¬n = n'e:{ objCount := n, nonIdCount := nc, comp := c, assoc := assoc✝¹ } =
{ objCount := n', nonIdCount := nc', comp := c', assoc := assoc✝ }⊢ n = n' All goals completed! 🐙))end FinCatend CategoryTheory