Grace/Cumulus/Category/Core.g17

Open in Workbench Download source

Imports

Algebra.Foundation · Set.Function · Set.Core

Declarations

Source

1-- Small categories as sets2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Category.Core8import Algebra.Foundation9import Set.Function10import Set.Core1112-- The composable pairs (g, f) of a set M of morphisms under domain and13-- codomain maps d and c: those with d(g) = c(f).14def composablePairsOf (M d c : Set) : Set :=15  { p ∈ M × M | ∃ g ∈ M, ∃ f ∈ M, p = (g, f) ∧ d(g) = c(f) }1617-- A small category is a structure of its objects, morphisms, domain and18-- codomain maps, identities, and composition. The projections read the data19-- back: C.obj and C.mor are the sets of objects and morphisms,20-- C.dom C.cod : C.mor → C.obj, C.id : C.obj → C.mor, and C.comp is a21-- function on the composable pairs (g, f) with C.dom(g) = C.cod(f), applied22-- as C.comp(g, f), read "g after f". Category(C) says that C is such a23-- structure whose data satisfy the laws below; Category.Data(C) is the24-- shape alone, and Category.intro builds a category from its fields.25structure Category26  | obj mor : Set27  | dom cod : mor → obj28  | id : obj → mor29  | comp : composablePairsOf(mor, dom, cod) → mor30  where31    identities : ∀ a ∈ obj, dom(id(a)) = a ∧ cod(id(a)) = a32    composites : ∀ g f ∈ mor, dom(g) = cod(f) →33      dom(comp(g, f)) = dom(f) ∧ cod(comp(g, f)) = cod(g)34    units : ∀ f ∈ mor, comp(id(cod(f)), f) = f ∧ comp(f, id(dom(f))) = f35    associative : ∀ h g f ∈ mor, dom(h) = cod(g) → dom(g) = cod(f) →36      comp(comp(h, g), f) = comp(h, comp(g, f))3738def composablePairs (C : Set) : Set := composablePairsOf(mor(C), dom(C), cod(C))3940theorem composablePairs.membership (C p : Set)41  shows p ∈ composablePairs(C) ↔ (p ∈ mor(C) × mor(C) ∧42    ∃ g ∈ mor(C), ∃ f ∈ mor(C), p = (g, f) ∧ dom(C)(g) = cod(C)(f))43proof44  simp [composablePairs]4546theorem composablePairs.mk (O M d c e m : Set)47  shows composablePairs(Category.mk(O, M, d, c, e, m)) = composablePairsOf(M, d, c)48proof49  simp [composablePairs, Category.mk.mor, Category.mk.dom, Category.mk.cod]5051theorem composablePairsOf.pair (M d c g f : Set)52  requires gInM : g ∈ M53  requires fInM : f ∈ M54  requires composable : d(g) = c(f)55  shows (g, f) ∈ composablePairsOf(M, d, c)56proof57  apply composablePairsOf.membership.backward58  constructor59  . exact product.pair with gInM, fInM60  . refine ⟨g, gInM, f, fInM, rfl, composable⟩6162theorem composablePairs.pair (C g f : Set)63  requires gInM : g ∈ mor(C)64  requires fInM : f ∈ mor(C)65  requires composable : dom(C)(g) = cod(C)(f)66  shows (g, f) ∈ composablePairs(C)67proof68  apply composablePairs.membership.backward69  constructor70  . exact product.pair with gInM, fInM71  . refine ⟨g, gInM, f, fInM, rfl, composable⟩7273theorem composablePairs.pair_iff (C g f : Set)74  shows (g, f) ∈ composablePairs(C) ↔75    (g ∈ mor(C) ∧ f ∈ mor(C) ∧ dom(C)(g) = cod(C)(f))76proof77  constructor78  . intro member79    obtain ⟨bounded, g2, g2InM, f2, f2InM, shape, composable⟩ :=80      composablePairs.membership.forward with member81    obtain ⟨gEqual, fEqual⟩ := orderedPair.injective with shape82    rw [gEqual, fEqual]83    refine ⟨g2InM, f2InM, composable⟩84  . intro h85    obtain ⟨gInM, fInM, composable⟩ := h86    exact composablePairs.pair with gInM, fInM, composable8788theorem composablePairs.subset (C : Set)89  shows composablePairs(C) ⊆ mor(C) × mor(C)90proof91  intros p member92  obtain ⟨bounded, rest⟩ := composablePairs.membership.forward with member93  exact bounded9495-- The projection laws of a constructed category as one rewrite set.96tactic category_projections := simp [Category.mk.obj, Category.mk.mor, Category.mk.dom, Category.mk.cod, Category.mk.comp, Category.mk.id, composablePairs.mk]9798-- Composition is written g ∘ f, read "g after f", wherever a hypothesis in99-- scope supplies the category; the operands' membership in mor(C) selects100-- the category when several are in scope.101notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis Category(C) for C.mor102103-- A morphism from a to b: a member of C.mor with domain a and codomain b.104-- Written f : a ⟶ b wherever a hypothesis in scope supplies the category.105-- The guard (f : a ⟶ b) on a binder makes f ∈ C.mor, C.dom(f) = a, and106-- C.cod(f) = b available to with *, simp, rw, and cc.107predicate Morphism (C f a b : Set) :=108  f ∈ C.mor ∧ C.dom(f) = a ∧ C.cod(f) = b109110notation mixfix "_ : _ ⟶ _" => Morphism(C, _, _, _) via hypothesis Category(C) for C.obj, C.mor111112-- The morphisms from a to b.113def hom (C a b : Set) : Set := { f ∈ mor(C) | dom(C)(f) = a ∧ cod(C)(f) = b }114115theorem hom.subset (C a b : Set)116  shows hom(C, a, b) ⊆ mor(C)117proof118  intros f member119  obtain ⟨fInM, rest⟩ := hom.membership.forward with member120  exact fInM121122theorem hom.dom (C a b f : Set)123  requires member : f ∈ hom(C, a, b)124  shows dom(C)(f) = a125proof126  obtain ⟨fInM, domF, codF⟩ := hom.membership.forward with member127  exact domF128129theorem hom.cod (C a b f : Set)130  requires member : f ∈ hom(C, a, b)131  shows cod(C)(f) = b132proof133  obtain ⟨fInM, domF, codF⟩ := hom.membership.forward with member134  exact codF135136theorem hom.in_morphisms (C a b f : Set)137  requires member : f ∈ hom(C, a, b)138  shows f ∈ mor(C)139proof140  obtain ⟨fInM, domF, codF⟩ := hom.membership.forward with member141  exact fInM142143theorem hom.of_morphism (C f : Set)144  requires fInM : f ∈ mor(C)145  shows f ∈ hom(C, dom(C)(f), cod(C)(f))146proof147  apply hom.membership.backward148  refine ⟨fInM, rfl, rfl⟩149150theorem hom.composable (C a b c g f : Set)151  requires gHom : g ∈ hom(C, b, c)152  requires fHom : f ∈ hom(C, a, b)153  shows dom(C)(g) = cod(C)(f)154proof155  have domG := hom.dom with gHom156  have codF := hom.cod with fHom157  cc158159-- Hom-sets with different endpoints are disjoint, and every morphism lies160-- in exactly one hom-set.161theorem hom.disjoint (C a b c d : Set)162  requires different : a ≠ c ∨ b ≠ d163  shows Disjoint(hom(C, a, b), hom(C, c, d))164proof165  unfold Disjoint166  ext f167  constructor168  . intro member169    obtain ⟨first, second⟩ := intersection.membership.forward with member170    obtain ⟨fInM, domA, codB⟩ := hom.membership.forward with first171    obtain ⟨fInM2, domC, codD⟩ := hom.membership.forward with second172    exfalso173    cases different with aDiff | bDiff174    . have same : a = c by cc175      exact aDiff with same176    . have same : b = d by cc177      exact bDiff with same178  . intro member179    exfalso180    exact set.empty with member181182theorem hom.unique_endpoints (C a b c d f : Set)183  requires first : f ∈ hom(C, a, b)184  requires second : f ∈ hom(C, c, d)185  shows a = c ∧ b = d186proof187  obtain ⟨fInM, domA, codB⟩ := hom.membership.forward with first188  obtain ⟨fInM2, domC, codD⟩ := hom.membership.forward with second189  constructor190  . cc191  . cc192193-- The guard Morphism(C, f, a, b) and the hom-set hom(C, a, b) say the same.194theorem Morphism.in_morphisms (C f a b : Set)195  requires fHom : Morphism(C, f, a, b)196  shows f ∈ mor(C)197proof198  obtain ⟨fInM, domF, codF⟩ := fHom199  exact fInM200201theorem Morphism.dom (C f a b : Set)202  requires fHom : Morphism(C, f, a, b)203  shows dom(C)(f) = a204proof205  obtain ⟨fInM, domF, codF⟩ := fHom206  exact domF207208theorem Morphism.cod (C f a b : Set)209  requires fHom : Morphism(C, f, a, b)210  shows cod(C)(f) = b211proof212  obtain ⟨fInM, domF, codF⟩ := fHom213  exact codF214215theorem Morphism.hom (C f a b : Set)216  requires fHom : Morphism(C, f, a, b)217  shows f ∈ hom(C, a, b)218proof219  unfold Morphism at fHom220  exact hom.membership.backward with fHom221222theorem Morphism.of_hom (C f a b : Set)223  requires member : f ∈ hom(C, a, b)224  shows Morphism(C, f, a, b)225proof226  unfold Morphism227  exact hom.membership.forward with member228229theorem Morphism.composable (C a b c f g : Set)230  requires fHom : Morphism(C, f, a, b)231  requires gHom : Morphism(C, g, b, c)232  shows dom(C)(g) = cod(C)(f)233proof234  obtain ⟨fInM, domF, codF⟩ := fHom235  obtain ⟨gInM, domG, codG⟩ := gHom236  cc237238section CategoryLaws239variable (C : Set)240hypothesis category : Category(C)241242theorem Category.dom_function243  shows dom(C) : mor(C) → obj(C)244proof245  simp [Category]246247theorem Category.cod_function248  shows cod(C) : mor(C) → obj(C)249proof250  simp [Category]251252theorem Category.id_function253  shows id(C) : obj(C) → mor(C)254proof255  simp [Category]256257theorem Category.comp_function258  shows comp(C) : composablePairs(C) → mor(C)259proof260  simp [Category, composablePairs]261262theorem Category.id_dom (a : Set)263  requires aInO : a ∈ obj(C)264  shows dom(C)(id(C)(a)) = a265proof266  rcases category with ⟨shape, domF, codF, idF, compF, idLaws, rest⟩267  obtain ⟨domLaw, codLaw⟩ := idLaws with a, aInO268  exact domLaw269270theorem Category.id_cod (a : Set)271  requires aInO : a ∈ obj(C)272  shows cod(C)(id(C)(a)) = a273proof274  rcases category with ⟨shape, domF, codF, idF, compF, idLaws, rest⟩275  obtain ⟨domLaw, codLaw⟩ := idLaws with a, aInO276  exact codLaw277278theorem Category.comp_dom (g f : Set)279  requires gInM : g ∈ mor(C)280  requires fInM : f ∈ mor(C)281  requires composable : dom(C)(g) = cod(C)(f)282  shows dom(C)(g ∘ f) = dom(C)(f)283proof284  rcases category with ⟨shape, domF, codF, idF, compF, idLaws, compLaws, rest⟩285  obtain ⟨domLaw, codLaw⟩ := compLaws with g, gInM, f, fInM, composable286  exact domLaw287288theorem Category.comp_cod (g f : Set)289  requires gInM : g ∈ mor(C)290  requires fInM : f ∈ mor(C)291  requires composable : dom(C)(g) = cod(C)(f)292  shows cod(C)(g ∘ f) = cod(C)(g)293proof294  rcases category with ⟨shape, domF, codF, idF, compF, idLaws, compLaws, rest⟩295  obtain ⟨domLaw, codLaw⟩ := compLaws with g, gInM, f, fInM, composable296  exact codLaw297298theorem Category.left_unit (f : Set)299  requires fInM : f ∈ mor(C)300  shows id(C)(cod(C)(f)) ∘ f = f301proof302  rcases category with303    ⟨shape, domF, codF, idF, compF, idLaws, compLaws, unitLaws, associative⟩304  obtain ⟨leftLaw, rightLaw⟩ := unitLaws with f, fInM305  exact leftLaw306307theorem Category.right_unit (f : Set)308  requires fInM : f ∈ mor(C)309  shows f ∘ id(C)(dom(C)(f)) = f310proof311  rcases category with312    ⟨shape, domF, codF, idF, compF, idLaws, compLaws, unitLaws, associative⟩313  obtain ⟨leftLaw, rightLaw⟩ := unitLaws with f, fInM314  exact rightLaw315316theorem Category.associative (h g f : Set)317  requires hInM : h ∈ mor(C)318  requires gInM : g ∈ mor(C)319  requires fInM : f ∈ mor(C)320  requires outer : dom(C)(h) = cod(C)(g)321  requires inner : dom(C)(g) = cod(C)(f)322  shows (h ∘ g) ∘ f = h ∘ (g ∘ f)323proof324  rcases category with325    ⟨shape, domF, codF, idF, compF, idLaws, compLaws, unitLaws, associative⟩326  exact associative with h, hInM, g, gInM, f, fInM, outer, inner327328theorem Category.dom_closed (f : Set)329  requires fInM : f ∈ mor(C)330  shows dom(C)(f) ∈ obj(C)331proof332  have function := Category.dom_function with category333  exact FunctionBetween.apply_closed with function, fInM334335theorem Category.cod_closed (f : Set)336  requires fInM : f ∈ mor(C)337  shows cod(C)(f) ∈ obj(C)338proof339  have function := Category.cod_function with category340  exact FunctionBetween.apply_closed with function, fInM341342theorem Category.id_closed (a : Set)343  requires aInO : a ∈ obj(C)344  shows id(C)(a) ∈ mor(C)345proof346  have function := Category.id_function with category347  exact FunctionBetween.apply_closed with function, aInO348349theorem Category.comp_closed (g f : Set)350  requires gInM : g ∈ mor(C)351  requires fInM : f ∈ mor(C)352  requires composable : dom(C)(g) = cod(C)(f)353  shows g ∘ f ∈ mor(C)354proof355  have function := Category.comp_function with category356  have pairIn := composablePairs.pair with gInM, fInM, composable357  unfold call2358  exact FunctionBetween.apply_closed with function, pairIn359360theorem Category.composable_pair_closed (p : Set)361  requires member : p ∈ composablePairs(C)362  shows comp(C)(p) ∈ mor(C)363proof364  have function := Category.comp_function with category365  exact FunctionBetween.apply_closed with function, member366367theorem Category.comp_value (g f : Set)368  shows comp(C)(g, f) = comp(C)((g, f))369proof370  unfold call2371  rfl372373-- Composition with an identity, stated at a named object.374theorem Category.id_left_of_cod (b f : Set)375  requires fInM : f ∈ mor(C)376  requires codF : cod(C)(f) = b377  shows id(C)(b) ∘ f = f378proof379  have law := Category.left_unit with category, fInM380  rwa codF at law381382theorem Category.id_right_of_dom (a f : Set)383  requires fInM : f ∈ mor(C)384  requires domF : dom(C)(f) = a385  shows f ∘ id(C)(a) = f386proof387  have law := Category.right_unit with category, fInM388  rwa domF at law389390theorem Category.id_id (a : Set)391  requires aInO : a ∈ obj(C)392  shows id(C)(a) ∘ id(C)(a) = id(C)(a)393proof394  have idInM := Category.id_closed with category, aInO395  have codId := Category.id_cod with category, aInO396  calc397    id(C)(a) ∘ id(C)(a) = id(C)(cod(C)(id(C)(a))) ∘ id(C)(a) := by rw codId398    _ = id(C)(a) := Category.left_unit with category, idInM399400theorem hom.id (a : Set)401  requires aInO : a ∈ obj(C)402  shows id(C)(a) ∈ hom(C, a, a)403proof404  have idInM := Category.id_closed with category, aInO405  have domId := Category.id_dom with category, aInO406  have codId := Category.id_cod with category, aInO407  apply hom.membership.backward408  refine ⟨idInM, domId, codId⟩409410theorem hom.comp (a b c g f : Set)411  requires gHom : g ∈ hom(C, b, c)412  requires fHom : f ∈ hom(C, a, b)413  shows g ∘ f ∈ hom(C, a, c)414proof415  obtain ⟨gInM, domG, codG⟩ := hom.membership.forward with gHom416  obtain ⟨fInM, domF, codF⟩ := hom.membership.forward with fHom417  have composable : dom(C)(g) = cod(C)(f) by cc418  have closed := Category.comp_closed with category, gInM, fInM, composable419  have domComp := Category.comp_dom with category, gInM, fInM, composable420  have codComp := Category.comp_cod with category, gInM, fInM, composable421  apply hom.membership.backward422  refine ⟨closed, ?_, ?_⟩423  . rwa domF at domComp424  . rwa codG at codComp425426theorem hom.exists_unique (f : Set)427  requires fInM : f ∈ mor(C)428  shows ∃ a ∈ obj(C), ∃ b ∈ obj(C), f ∈ hom(C, a, b) ∧429    (∀ c, ∀ d, f ∈ hom(C, c, d) → c = a ∧ d = b)430proof431  have domIn := Category.dom_closed with category, fInM432  have codIn := Category.cod_closed with category, fInM433  have member := hom.of_morphism at C, f with fInM434  refine ⟨dom(C)(f), domIn, cod(C)(f), codIn, member, ?_⟩435  intros c d other436  obtain ⟨fInM2, domC, codD⟩ := hom.membership.forward with other437  constructor438  . symm439    exact domC440  . symm441    exact codD442443theorem hom.union_is_morphisms (f : Set)444  shows f ∈ mor(C) ↔ ∃ a ∈ obj(C), ∃ b ∈ obj(C), f ∈ hom(C, a, b)445proof446  constructor447  . intro fInM448    have domIn := Category.dom_closed with category, fInM449    have codIn := Category.cod_closed with category, fInM450    have member := hom.of_morphism at C, f with fInM451    refine ⟨dom(C)(f), domIn, cod(C)(f), codIn, member⟩452  . intro h453    obtain ⟨a, aInO, b, bInO, member⟩ := h454    exact hom.in_morphisms with member455456-- The endpoints of a composite, in hom-set form.457theorem Category.comp_dom_cod (a b c g f : Set)458  requires gHom : g ∈ hom(C, b, c)459  requires fHom : f ∈ hom(C, a, b)460  shows dom(C)(g ∘ f) = a ∧ cod(C)(g ∘ f) = c461proof462  have composite := hom.comp with category, gHom, fHom463  obtain ⟨inM, domC, codC⟩ := hom.membership.forward with composite464  refine ⟨domC, codC⟩465466-- Associativity and the unit laws in hom-set form.467theorem Category.assoc_hom (a b c d h g f : Set)468  requires hHom : h ∈ hom(C, c, d)469  requires gHom : g ∈ hom(C, b, c)470  requires fHom : f ∈ hom(C, a, b)471  shows (h ∘ g) ∘ f = h ∘ (g ∘ f)472proof473  have hInM := hom.in_morphisms with hHom474  have gInM := hom.in_morphisms with gHom475  have fInM := hom.in_morphisms with fHom476  have outer := hom.composable with hHom, gHom477  have inner := hom.composable with gHom, fHom478  exact Category.associative with category, hInM, gInM, fInM, outer, inner479480theorem Category.id_left_hom (a b f : Set)481  requires fHom : f ∈ hom(C, a, b)482  shows id(C)(b) ∘ f = f483proof484  have fInM := hom.in_morphisms with fHom485  have codF := hom.cod with fHom486  exact Category.id_left_of_cod with category, fInM, codF487488theorem Category.id_right_hom (a b f : Set)489  requires fHom : f ∈ hom(C, a, b)490  shows f ∘ id(C)(a) = f491proof492  have fInM := hom.in_morphisms with fHom493  have domF := hom.dom with fHom494  exact Category.id_right_of_dom with category, fInM, domF495496-- An endomorphism that acts as a two-sided unit is the identity.497theorem Category.id_unique (a e : Set)498  requires aInO : a ∈ obj(C)499  requires eHom : e ∈ hom(C, a, a)500  requires unit : ∀ f ∈ mor(C), dom(C)(f) = a → f ∘ e = f501  shows e = id(C)(a)502proof503  have idInM := Category.id_closed with category, aInO504  have domId := Category.id_dom with category, aInO505  have leftUnit := Category.id_left_hom with category, eHom506  calc507    e = id(C)(a) ∘ e := by rw leftUnit508    _ = id(C)(a) := unit with id(C)(a), idInM, domId509510theorem Category.id_unique_left (a e : Set)511  requires aInO : a ∈ obj(C)512  requires eHom : e ∈ hom(C, a, a)513  requires unit : ∀ f ∈ mor(C), cod(C)(f) = a → e ∘ f = f514  shows e = id(C)(a)515proof516  have idInM := Category.id_closed with category, aInO517  have codId := Category.id_cod with category, aInO518  have rightUnit := Category.id_right_hom with category, eHom519  calc520    e = e ∘ id(C)(a) := by rw rightUnit521    _ = id(C)(a) := unit with id(C)(a), idInM, codId522523-- The endomorphisms of an object form a monoid under composition.524theorem Category.endomorphism_closed (a g f : Set)525  requires gHom : g ∈ hom(C, a, a)526  requires fHom : f ∈ hom(C, a, a)527  shows g ∘ f ∈ hom(C, a, a)528proof529  exact hom.comp with category, gHom, fHom530531theorem Category.objects_nonempty_of_morphism (f : Set)532  requires fInM : f ∈ mor(C)533  shows Nonempty(obj(C))534proof535  have domIn := Category.dom_closed with category, fInM536  refine ⟨dom(C)(f), domIn⟩537538theorem Category.morphisms_nonempty_of_object (a : Set)539  requires aInO : a ∈ obj(C)540  shows Nonempty(mor(C))541proof542  have idIn := Category.id_closed with category, aInO543  refine ⟨id(C)(a), idIn⟩544545theorem Category.id_injective (a b : Set)546  requires aInO : a ∈ obj(C)547  requires bInO : b ∈ obj(C)548  requires same : id(C)(a) = id(C)(b)549  shows a = b550proof551  have domA := Category.id_dom with category, aInO552  have domB := Category.id_dom with category, bInO553  cc554555-- Typing morphisms by their endpoints.556theorem Morphism.of_morphism (f : Set)557  requires fInM : f ∈ mor(C)558  shows f : dom(C)(f) ⟶ cod(C)(f)559proof560  unfold Morphism561  refine ⟨fInM, rfl, rfl⟩562563theorem Morphism.of_composable (g f : Set)564  requires gInM : g ∈ mor(C)565  requires fInM : f ∈ mor(C)566  requires composable : dom(C)(g) = cod(C)(f)567  shows g : cod(C)(f) ⟶ cod(C)(g)568proof569  unfold Morphism570  refine ⟨gInM, composable, rfl⟩571572theorem Morphism.of_dom_cod (f a b : Set)573  requires fInM : f ∈ mor(C)574  requires domF : dom(C)(f) = a575  requires codF : cod(C)(f) = b576  shows f : a ⟶ b577proof578  unfold Morphism579  refine ⟨fInM, domF, codF⟩580581theorem Morphism.dom_object (a b : Set) (f : a ⟶ b)582  shows a ∈ obj(C)583proof584  have domIn : dom(C)(f) ∈ obj(C) := Category.dom_closed with *585  have domF : dom(C)(f) = a by cc586  rwa domF at domIn587588theorem Morphism.cod_object (a b : Set) (f : a ⟶ b)589  shows b ∈ obj(C)590proof591  have codIn : cod(C)(f) ∈ obj(C) := Category.cod_closed with *592  have codF : cod(C)(f) = b by cc593  rwa codF at codIn594595instance Morphism.id (a : Set)596  requires aInO : a ∈ obj(C)597  shows id(C)(a) : a ⟶ a598proof599  have idInM := Category.id_closed with category, aInO600  have domId := Category.id_dom with category, aInO601  have codId := Category.id_cod with category, aInO602  unfold Morphism603  refine ⟨idInM, domId, codId⟩604605instance Morphism.comp (a b c : Set) (f : a ⟶ b) (g : b ⟶ c)606  shows g ∘ f : a ⟶ c607proof608  have composable : dom(C)(g) = cod(C)(f) by cc609  have closed : g ∘ f ∈ mor(C) := Category.comp_closed with *610  have domComp : dom(C)(g ∘ f) = dom(C)(f) := Category.comp_dom with *611  have codComp : cod(C)(g ∘ f) = cod(C)(g) := Category.comp_cod with *612  unfold Morphism613  refine ⟨closed, ?_, ?_⟩614  . cc615  . cc616617-- The unit laws and associativity, stated on hom-typed binders.618theorem Category.id_left (a b : Set) (f : a ⟶ b)619  shows id(C)(b) ∘ f = f620proof621  have codF : cod(C)(f) = b by cc622  have law : id(C)(cod(C)(f)) ∘ f = f := Category.left_unit with *623  rwa codF at law624625theorem Category.id_right (a b : Set) (f : a ⟶ b)626  shows f ∘ id(C)(a) = f627proof628  have domF : dom(C)(f) = a by cc629  have law : f ∘ id(C)(dom(C)(f)) = f := Category.right_unit with *630  rwa domF at law631632theorem Category.assoc (a b c d : Set) (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d)633  shows (h ∘ g) ∘ f = h ∘ (g ∘ f)634proof635  have outer : dom(C)(h) = cod(C)(g) by cc636  have inner : dom(C)(g) = cod(C)(f) by cc637  exact Category.associative with *638639end CategoryLaws640641-- The categorical rewrite set: the unit laws and associativity, each642-- applied where the hom guards of its morphisms are in scope.643tactic category_simp := simp [Category.id_left, Category.id_right, Category.assoc]644