1. Geb
  2. Mathlib
  3. CategoryTheory
  4. FinCat
  5. Hom
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.Category public import Mathlib.CategoryTheory.Functor.Basic

Functor specifications

A functor between two finite-category specifications is specified by a map on object indices, a map on client morphisms, and a Bool equation asserting preservation of composition. The client morphism map lands in the target's full hom type, a functor being free to send a non-identity morphism to an identity. Preservation of identities is not checked: the extension of the morphism map to the full hom types sends the reserved identity to the reserved identity by construction.

Functor specifications compose, and the identity and composition satisfy the unit and associativity laws as equalities of specifications, not merely up to isomorphism.

Main definitions

    CategoryTheory.FinCat.Hom.mapTotalOf, CategoryTheory.FinCat.Hom.mapTotal — the extension of the morphism map to the full hom types.

    CategoryTheory.FinCat.Hom.compCheckOf, CategoryTheory.FinCat.Hom.compCheck — the decidable preservation-of-composition check on pairs of client morphisms.

    CategoryTheory.FinCat.Hom — the functor specification type.

    CategoryTheory.FinCat.Hom.id, CategoryTheory.FinCat.Hom.comp — the identity specification and composition of specifications.

    CategoryTheory.FinCat.Hom.toFunctor — the mathlib functor a specification generates.

Main statements

    FinCat.Hom.compCheck_eq_true_iff — the check reflects preservation of composition on pairs of client morphisms.

    FinCat.Hom.mapTotal_emb, FinCat.Hom.mapTotal_id — the total map on a client morphism and on the reserved identity.

    FinCat.Hom.mapTotal_compTotal — preservation of composition, on all pairs of morphisms.

    FinCat.Hom.id_mapTotalOf, FinCat.Hom.comp_mapTotalOf, FinCat.Hom.id_mapTotal, FinCat.Hom.comp_mapTotal — the total map of the identity and of a composite.

    FinCat.Hom.id_comp, FinCat.Hom.comp_id, FinCat.Hom.assoc — the unit and associativity laws, as equalities.

Implementation notes

mapTotalOf and compCheckOf precede the structure because the compValid field's type mentions them. The enclosing namespace FinCat stays open throughout; the inner namespace Hom block closes before structure Hom, which cannot be declared inside a namespace of its own name, and reopens after.

The check is stated over the total composition and the total morphism map rather than over the client data alone: a composite of two client morphisms may land on the reserved identity index, on which the client's morphism map is undefined.

mapTotal_compTotal extends the check off the client range. The extension, rather than the check itself, is what the composite of two functor specifications needs: its validity field is the outer specification's preservation of composition at two morphisms of the form mapTotal (emb _), which need not be embedded client morphisms of the middle specification.

id_mapTotalOf and comp_mapTotalOf are stated about mapTotalOf applied to given data rather than about a specification, because FinCat.Hom.id and FinCat.Hom.comp consume them to discharge their own validity fields. id_mapTotal and comp_mapTotal are the corresponding statements about the specifications those two build.

The unit and associativity laws go through the heterogeneous ext lemma: the objMap components agree definitionally, so the HEq of the map components is an equality, and the compValid components are proof-irrelevant.

References

    [JohnsonYau2021] § 1.1 — the notion of functor, of which this module's specification type is a presentation.

Tags

category, functor, finite category, decidable, constructive, choice-free

@[expose] public sectionnamespace CategoryTheorynamespace FinCatnamespace Hom

The extension of a functor specification's morphism map to the full hom types, sending the reserved identity to the reserved identity. The identity branch's bound needs i = j, which eq_of_nonIdCount_le supplies; the value component crosses with no Eq.rec.

def mapTotalOf {S T : FinCat} (objMap : Fin S.objCount → Fin T.objCount) (map : (i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)) {i j : Fin S.objCount} (x : S.Mor i j) : T.Mor (objMap i) (objMap j) := if hx : x.val < S.nonIdCount i j then map i j ⟨x.val, hx⟩ else ⟨(T.id (objMap i)).val, S:FinCatT:FinCatobjMap:Fin S.objCount → Fin T.objCountmap:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)i:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ ↑(T.id (objMap i)) < T.homCount (objMap i) (objMap j) S:FinCatT:FinCatobjMap:Fin S.objCount → Fin T.objCountmap:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)i:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i jhij:i = j⊢ ↑(T.id (objMap i)) < T.homCount (objMap i) (objMap j) S:FinCatT:FinCatobjMap:Fin S.objCount → Fin T.objCountmap:(i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)i:Fin S.objCountx:S.Mor i ihx:¬↑x < S.nonIdCount i i⊢ ↑(T.id (objMap i)) < T.homCount (objMap i) (objMap i) All goals completed! 🐙⟩

Preservation of composition, as a Bool, on pairs of client morphisms. Stated over the total composition and the total morphism map: a client composite may land on the reserved index, on which the partial map is undefined.

def compCheckOf (S T : FinCat) (objMap : Fin S.objCount → Fin T.objCount) (map : (i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)) : Bool := decide <| ∀ (i j k : Fin S.objCount) (f : Fin (S.nonIdCount i j)) (g : Fin (S.nonIdCount j k)), mapTotalOf objMap map (S.compTotal (S.emb f) (S.emb g)) = T.compTotal (mapTotalOf objMap map (S.emb f)) (mapTotalOf objMap map (S.emb g))
end Hom

A functor specification between two finite-category specifications. FinCat.Hom is named for its position — the 1-cells of a 2-category — not for its shape: unlike CategoryTheory.Cat.Hom it is not a one-field bundling.

The map on object indices.

The map on client morphisms. It lands in the target's full hom type, since a functor may send a non-identity morphism to an identity; every functor into the terminal category does.

Preservation of composition.

@[ext] structure Hom (S T : FinCat) where objMap : Fin S.objCount → Fin T.objCount map : (i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j) compValid : Hom.compCheckOf S T objMap map = true
namespace Homvariable {S T : FinCat}

The composition check reflects preservation of composition on pairs of client morphisms.

theorem compCheck_eq_true_iff (S T : FinCat) (objMap : Fin S.objCount → Fin T.objCount) (map : (i j : Fin S.objCount) → Fin (S.nonIdCount i j) → T.Mor (objMap i) (objMap j)) : compCheckOf S T objMap map = true ↔ ∀ (i j k : Fin S.objCount) (f : Fin (S.nonIdCount i j)) (g : Fin (S.nonIdCount j k)), mapTotalOf objMap map (S.compTotal (S.emb f) (S.emb g)) = T.compTotal (mapTotalOf objMap map (S.emb f)) (mapTotalOf objMap map (S.emb g)) := decide_eq_true_iff

F on the full hom types.

def mapTotal (F : Hom S T) {i j : Fin S.objCount} (x : S.Mor i j) : T.Mor (F.objMap i) (F.objMap j) := mapTotalOf F.objMap F.map x

F's composition check.

def compCheck (F : Hom S T) : Bool := compCheckOf S T F.objMap F.map

On an embedded client morphism the total map is the client map.

theorem mapTotal_emb (F : Hom S T) {i j : Fin S.objCount} (f : Fin (S.nonIdCount i j)) : F.mapTotal (S.emb f) = F.map i j f := S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountf:Fin (S.nonIdCount i j)⊢ F.mapTotal (emb f) = F.map i j f S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountf:Fin (S.nonIdCount i j)hlt:↑(emb f) < S.nonIdCount i j⊢ F.mapTotal (emb f) = F.map i j f S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountf:Fin (S.nonIdCount i j)hlt:↑(emb f) < S.nonIdCount i j⊢ (if hx : ↑(emb f) < S.nonIdCount i j then F.map i j ⟨↑(emb f), hx⟩ else ⟨↑(T.id (F.objMap i)), ⋯⟩) = F.map i j f S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountf:Fin (S.nonIdCount i j)hlt:↑(emb f) < S.nonIdCount i j⊢ F.map i j ⟨↑(emb f), hlt⟩ = F.map i j f All goals completed! 🐙

The total map preserves the reserved identity.

theorem mapTotal_id (F : Hom S T) (i : Fin S.objCount) : F.mapTotal (S.id i) = T.id (F.objMap i) := S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCount⊢ F.mapTotal (S.id i) = T.id (F.objMap i) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCounthlt:¬↑(S.id i) < S.nonIdCount i i⊢ F.mapTotal (S.id i) = T.id (F.objMap i) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCounthlt:¬↑(S.id i) < S.nonIdCount i i⊢ (if hx : ↑(S.id i) < S.nonIdCount i i then F.map i i ⟨↑(S.id i), hx⟩ else ⟨↑(T.id (F.objMap i)), ⋯⟩) = T.id (F.objMap i) All goals completed! 🐙

The total map preserves the total composition, on all pairs of morphisms.

theorem mapTotal_compTotal (F : Hom S T) {i j k : Fin S.objCount} (x : S.Mor i j) (y : S.Mor j k) : F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) := S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y)S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:¬↑x < S.nonIdCount i j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i jhy:↑y < S.nonIdCount j k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y)S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i jhy:¬↑y < S.nonIdCount j k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i jhy:↑y < S.nonIdCount j k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) All goals completed! 🐙 S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i jhy:¬↑y < S.nonIdCount j k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:↑x < S.nonIdCount i jhy:¬↑y < S.nonIdCount j khjk:j = k⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i jy:S.Mor j jhy:¬↑y < S.nonIdCount j j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) All goals completed! 🐙 S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:¬↑x < S.nonIdCount i j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountj:Fin S.objCountk:Fin S.objCountx:S.Mor i jy:S.Mor j khx:¬↑x < S.nonIdCount i jhij:i = j⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) S:FinCatT:FinCatF:S.Hom Ti:Fin S.objCountk:Fin S.objCountx:S.Mor i iy:S.Mor i khx:¬↑x < S.nonIdCount i i⊢ F.mapTotal (S.compTotal x y) = T.compTotal (F.mapTotal x) (F.mapTotal y) All goals completed! 🐙

mapTotalOf at the identity 1-cell's data is the identity.

theorem id_mapTotalOf (S : FinCat) {i j : Fin S.objCount} (x : S.Mor i j) : mapTotalOf (fun i ↦ i) (fun _ _ f ↦ S.emb f) x = x := S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i j⊢ mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) x = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i j⊢ (if hx : ↑x < S.nonIdCount i j then (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ else ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩) = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i j⊢ (if hx : ↑x < S.nonIdCount i j then (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ else ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩) = xS:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ (if hx : ↑x < S.nonIdCount i j then (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ else ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩) = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i j⊢ (if hx : ↑x < S.nonIdCount i j then (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ else ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩) = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i j⊢ (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ = x All goals completed! 🐙 S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ (if hx : ↑x < S.nonIdCount i j then (fun x x_1 f ↦ emb f) i j ⟨↑x, hx⟩ else ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩) = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩ = x S:FinCati:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i jhij:i = j⊢ ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩ = x S:FinCati:Fin S.objCountx:S.Mor i ihx:¬↑x < S.nonIdCount i i⊢ ⟨↑(S.id ((fun i ↦ i) i)), ⋯⟩ = x All goals completed! 🐙

mapTotalOf at a composite's data factors as the outer 1-cell applied to the inner.

theorem comp_mapTotalOf {S T U : FinCat} (F : Hom S T) (G : Hom T U) {i j : Fin S.objCount} (x : S.Mor i j) : mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) := S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x)S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i jh1:mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.map i j ⟨↑x, hx⟩)⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:↑x < S.nonIdCount i jh1:mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.map i j ⟨↑x, hx⟩)h2:F.mapTotal x = F.map i j ⟨↑x, hx⟩⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) All goals completed! 🐙 S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountx:S.Mor i jhx:¬↑x < S.nonIdCount i jhij:i = j⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountx:S.Mor i ihx:¬↑x < S.nonIdCount i i⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) x = G.mapTotal (F.mapTotal x) S:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountx:S.Mor i ihx:¬↑x < S.nonIdCount i i⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (S.id i) = U.id (G.objMap (F.objMap i)) All goals completed! 🐙

The identity 1-cell.

protected def id (S : FinCat) : Hom S S where objMap := fun i ↦ i map := fun _ _ f ↦ S.emb f compValid := S✝:FinCatT:FinCatS:FinCat⊢ (compCheckOf S S (fun i ↦ i) fun x x_1 f ↦ emb f) = true S✝:FinCatT:FinCatS:FinCat⊢ ∀ (i j k : Fin S.objCount) (f : Fin (S.nonIdCount i j)) (g : Fin (S.nonIdCount j k)), mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (S.compTotal (emb f) (emb g)) = S.compTotal (mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (emb f)) (mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (emb g)) S✝:FinCatT:FinCatS:FinCati:Fin S.objCountj:Fin S.objCountk:Fin S.objCountf:Fin (S.nonIdCount i j)g:Fin (S.nonIdCount j k)⊢ mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (S.compTotal (emb f) (emb g)) = S.compTotal (mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (emb f)) (mapTotalOf (fun i ↦ i) (fun x x_1 f ↦ emb f) (emb g)) All goals completed! 🐙

Composition of 1-cells.

def comp {S T U : FinCat} (F : Hom S T) (G : Hom T U) : Hom S U where objMap := fun i ↦ G.objMap (F.objMap i) map := fun i j f ↦ G.mapTotal (F.map i j f) compValid := S✝:FinCatT✝:FinCatS:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom U⊢ (compCheckOf S U (fun i ↦ G.objMap (F.objMap i)) fun i j f ↦ G.mapTotal (F.map i j f)) = true S✝:FinCatT✝:FinCatS:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom U⊢ ∀ (i j k : Fin S.objCount) (f : Fin (S.nonIdCount i j)) (g : Fin (S.nonIdCount j k)), mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (S.compTotal (emb f) (emb g)) = U.compTotal (mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (emb f)) (mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (emb g)) S✝:FinCatT✝:FinCatS:FinCatT:FinCatU:FinCatF:S.Hom TG:T.Hom Ui:Fin S.objCountj:Fin S.objCountk:Fin S.objCountf:Fin (S.nonIdCount i j)g:Fin (S.nonIdCount j k)⊢ mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (S.compTotal (emb f) (emb g)) = U.compTotal (mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (emb f)) (mapTotalOf (fun i ↦ G.objMap (F.objMap i)) (fun i j f ↦ G.mapTotal (F.map i j f)) (emb g)) All goals completed! 🐙

The identity 1-cell acts as the identity on total morphisms.

theorem id_mapTotal (S : FinCat) {i j : Fin S.objCount} (x : S.Mor i j) : (Hom.id S).mapTotal x = x := id_mapTotalOf S x

A composite 1-cell's total map factors.

theorem comp_mapTotal {S T U : FinCat} (F : Hom S T) (G : Hom T U) {i j : Fin S.objCount} (x : S.Mor i j) : (F.comp G).mapTotal x = G.mapTotal (F.mapTotal x) := comp_mapTotalOf F G x

The identity 1-cell is a left identity, on the nose.

theorem id_comp {S T : FinCat} (F : Hom S T) : (Hom.id S).comp F = F := Hom.ext rfl (heq_of_eq (funext fun _ ↦ funext fun _ ↦ funext fun f ↦ F.mapTotal_emb f))

The identity 1-cell is a right identity, on the nose.

theorem comp_id {S T : FinCat} (F : Hom S T) : F.comp (Hom.id T) = F := Hom.ext rfl (heq_of_eq (funext fun i ↦ funext fun j ↦ funext fun f ↦ id_mapTotal T (F.map i j f)))

1-cell composition is associative, on the nose.

theorem assoc {S T U V : FinCat} (F : Hom S T) (G : Hom T U) (H : Hom U V) : (F.comp G).comp H = F.comp (G.comp H) := Hom.ext rfl (heq_of_eq (funext fun i ↦ funext fun j ↦ funext fun f ↦ (comp_mapTotal G H (F.map i j f)).symm))

The mathlib functor a functor specification generates. The type is written with explicit instance arguments rather than through ⥤, so that v appears in it and is not left to be inferred from a hidden instance argument.

def toFunctor.{v, u} {S T : FinCat} (F : Hom S T) : @Functor (Obj.{u} S) (Obj.category.{v, u} S) (Obj.{u} T) (Obj.category.{v, u} T) where obj X := ⟨ULift.up (F.objMap X.idx.down)⟩ map f := ULift.up (F.mapTotal f.down) map_id _ := congrArg ULift.up (F.mapTotal_id _) map_comp _ _ := congrArg ULift.up (F.mapTotal_compTotal _ _)
end Homend FinCatend CategoryTheory