Grace/Cumulus/Category/Opposite.g17

Open in Workbench Download source

Imports

Natural

Declarations

Source

1-- The opposite category2-- 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.Opposite8import Natural910-- The opposite category keeps the objects and morphisms, swaps dom and11-- cod, and composes in the reverse order: the opposite composite of12-- (g, f) with cod(C)(g) = dom(C)(f) is comp(C)(f, g).13def oppositePairs (C : Set) : Set := composablePairsOf(mor(C), cod(C), dom(C))1415def oppositeComposition (C : Set) : Set :=16  { p ∈ oppositePairs(C) × mor(C) |17    ∃ g ∈ mor(C), ∃ f ∈ mor(C), p = ((g, f) ↦ comp(C)(f, g)) ∧18      cod(C)(g) = dom(C)(f) }1920def opposite (C : Set) : Set :=21  Category.mk(Category.obj(C), mor(C), cod(C), dom(C), id(C), oppositeComposition(C))2223theorem oppositePairs.membership (C p : Set)24  shows p ∈ oppositePairs(C) ↔ (p ∈ mor(C) × mor(C) ∧25    ∃ g ∈ mor(C), ∃ f ∈ mor(C), p = (g, f) ∧ cod(C)(g) = dom(C)(f))26proof27  simp [oppositePairs]2829theorem oppositePairs.pair (C g f : Set)30  requires gInM : g ∈ mor(C)31  requires fInM : f ∈ mor(C)32  requires composable : cod(C)(g) = dom(C)(f)33  shows (g, f) ∈ oppositePairs(C)34proof35  apply oppositePairs.membership.backward36  constructor37  . exact product.pair with gInM, fInM38  . refine ⟨g, gInM, f, fInM, rfl, composable⟩3940theorem opposite.obj (C : Set)41  shows obj(opposite(C)) = Category.obj(C)42proof43  simp [opposite, Category.mk.obj]4445theorem opposite.mor (C : Set)46  shows mor(opposite(C)) = mor(C)47proof48  simp [opposite, Category.mk.mor]4950theorem opposite.dom (C : Set)51  shows dom(opposite(C)) = cod(C)52proof53  simp [opposite, Category.mk.dom]5455theorem opposite.cod (C : Set)56  shows cod(opposite(C)) = dom(C)57proof58  simp [opposite, Category.mk.cod]5960theorem opposite.comp (C : Set)61  shows comp(opposite(C)) = oppositeComposition(C)62proof63  simp [opposite, Category.mk.comp]6465theorem opposite.id (C : Set)66  shows id(opposite(C)) = id(C)67proof68  simp [opposite, Category.mk.id]6970theorem opposite.projections (C : Set)71  shows obj(opposite(C)) = Category.obj(C) ∧ mor(opposite(C)) = mor(C) ∧72    dom(opposite(C)) = cod(C) ∧ cod(opposite(C)) = dom(C) ∧73    comp(opposite(C)) = oppositeComposition(C) ∧ id(opposite(C)) = id(C)74proof75  refine ⟨opposite.obj at C, opposite.mor at C, opposite.dom at C, opposite.cod at C,76    opposite.comp at C, opposite.id at C⟩7778-- The projections of the opposite as one rewrite set, for equational goals.79tactic opposite_projections := simp [opposite.obj, opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id]8081theorem composablePairs.opposite (C : Set)82  shows composablePairs(opposite(C)) = oppositePairs(C)83proof84  simp [composablePairs, oppositePairs, opposite.mor, opposite.dom, opposite.cod]8586theorem oppositePairs.opposite (C : Set)87  shows oppositePairs(opposite(C)) = composablePairs(C)88proof89  simp [composablePairs, oppositePairs, opposite.mor, opposite.dom, opposite.cod]9091-- Hom-sets of the opposite are the reversed hom-sets.92theorem hom.opposite (C a b : Set)93  shows hom(opposite(C), a, b) = hom(C, b, a)94proof95  ext f96  constructor97  . intro member98    obtain ⟨fInM, codF, domF⟩ := hom.membership.forward with member99    simp [opposite.obj, opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id] at fInM100    simp [opposite.obj, opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id] at codF101    simp [opposite.obj, opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id] at domF102    apply hom.membership.backward103    refine ⟨fInM, domF, codF⟩104  . intro member105    obtain ⟨fInM, domF, codF⟩ := hom.membership.forward with member106    apply hom.membership.backward107    rw [opposite.mor, opposite.dom, opposite.cod]108    refine ⟨fInM, codF, domF⟩109110section OppositeLaws111variable (C : Set)112hypothesis category : Category(C)113114theorem oppositeComposition.relates (g f : Set)115  requires gInM : g ∈ mor(C)116  requires fInM : f ∈ mor(C)117  requires composable : cod(C)(g) = dom(C)(f)118  shows relates(oppositeComposition(C), (g, f), f ∘ g)119proof120  have reversed : dom(C)(f) = cod(C)(g) by cc121  have valueIn := Category.comp_closed with category, fInM, gInM, reversed122  have pairIn := oppositePairs.pair with gInM, fInM, composable123  unfold relates124  apply oppositeComposition.membership.backward125  constructor126  . exact product.pair with pairIn, valueIn127  . refine ⟨g, gInM, f, fInM, rfl, composable⟩128129theorem oppositeComposition.function130  shows oppositeComposition(C) : oppositePairs(C) → mor(C)131proof132  unfold FunctionBetween133  refine ⟨?_, ?_, ?_⟩134  . intros p member135    obtain ⟨bounded, rest⟩ := oppositeComposition.membership.forward with member136    exact bounded137  . intros x y xy z xz138    unfold relates at xy139    obtain ⟨_, g, gInM, f, fInM, firstShape, firstComposable⟩ :=140      oppositeComposition.membership.forward with xy141    unfold relates at xz142    obtain ⟨_, k, kInM, h, hInM, secondShape, secondComposable⟩ :=143      oppositeComposition.membership.forward with xz144    obtain ⟨firstPair, yValue⟩ := orderedPair.injective with firstShape145    obtain ⟨secondPair, zValue⟩ := orderedPair.injective with secondShape146    have samePair : (g, f) = (k, h) by cc147    obtain ⟨gk, fh⟩ := orderedPair.injective with samePair148    cc149  . intros p member150    obtain ⟨bounded, g, gInM, f, fInM, shape, composable⟩ :=151      oppositePairs.membership.forward with member152    have reversed : dom(C)(f) = cod(C)(g) by cc153    have valueIn := Category.comp_closed with category, fInM, gInM, reversed154    have related := oppositeComposition.relates with155      category, gInM, fInM, composable156    refine ⟨f ∘ g, valueIn, ?_⟩157    rw shape158    exact related159160theorem oppositeComposition.apply (g f : Set)161  requires gInM : g ∈ mor(C)162  requires fInM : f ∈ mor(C)163  requires composable : cod(C)(g) = dom(C)(f)164  shows oppositeComposition(C)(g, f) = f ∘ g165proof166  have function := oppositeComposition.function with category167  have pairIn := oppositePairs.pair with gInM, fInM, composable168  have related := oppositeComposition.relates with169    category, gInM, fInM, composable170  have value := FunctionBetween.apply_value with function, pairIn, related171  simp [call2]172173theorem Category.opposite174  shows Category(opposite(C))175proof176  have domF := Category.dom_function with category177  have codF := Category.cod_function with category178  have idF := Category.id_function with category179  have compF := oppositeComposition.function with category180  have shape : Category.Data(opposite(C)) by simp [opposite, Category.mk.data]181  have pairs : composablePairsOf(mor(C), cod(C), dom(C)) = oppositePairs(C)182    have reversed := composablePairs.opposite at C183    simp [composablePairs, opposite.mor, opposite.dom, opposite.cod] at reversed184    exact reversed185  obtain ⟨objE, morE, domE, codE, compE, idE⟩ := opposite.projections at C186  unfold Category187  rw under objE188  rw under morE189  rw under domE190  rw under codE191  rw under compE192  rw under idE193  rw pairs194  refine ⟨shape, codF, domF, idF, compF, ?_, ?_, ?_, ?_⟩195  . intros a aInO196    have domId := Category.id_dom with category, aInO197    have codId := Category.id_cod with category, aInO198    refine ⟨codId, domId⟩199  . intros g gInM f fInM composable200    have value := oppositeComposition.apply with201      category, gInM, fInM, composable202    have reversed : dom(C)(f) = cod(C)(g) by cc203    have domValue := Category.comp_dom with category, fInM, gInM, reversed204    have codValue := Category.comp_cod with category, fInM, gInM, reversed205    rw value206    refine ⟨codValue, domValue⟩207  . intros f fInM208    have domIn := Category.dom_closed with category, fInM209    have codIn := Category.cod_closed with category, fInM210    have idDomIn := Category.id_closed with category, domIn211    have idCodIn := Category.id_closed with category, codIn212    have domIdCod := Category.id_cod with category, domIn213    have codIdDom := Category.id_dom with category, codIn214    have leftComposable : cod(C)(id(C)(dom(C)(f))) = dom(C)(f) by cc215    have rightComposable : cod(C)(f) = dom(C)(id(C)(cod(C)(f))) by cc216    have leftValue := oppositeComposition.apply with217      category, idDomIn, fInM, leftComposable218    have rightValue := oppositeComposition.apply with219      category, fInM, idCodIn, rightComposable220    have leftUnit := Category.left_unit with category, fInM221    have rightUnit := Category.right_unit with category, fInM222    rw [leftValue, rightValue]223    refine ⟨rightUnit, leftUnit⟩224  . intros h hInM g gInM f fInM outer inner225    have gh : dom(C)(g) = cod(C)(h) by cc226    have fg : dom(C)(f) = cod(C)(g) by cc227    have ghIn := Category.comp_closed with category, gInM, hInM, gh228    have fgIn := Category.comp_closed with category, fInM, gInM, fg229    have codGH := Category.comp_cod with category, gInM, hInM, gh230    have domFG := Category.comp_dom with category, fInM, gInM, fg231    have hgValue := oppositeComposition.apply with category, hInM, gInM, outer232    have gfValue := oppositeComposition.apply with category, gInM, fInM, inner233    have outerComposable : cod(C)(g ∘ h) = dom(C)(f) by cc234    have innerComposable : cod(C)(h) = dom(C)(f ∘ g) by cc235    have leftValue := oppositeComposition.apply with236      category, ghIn, fInM, outerComposable237    have rightValue := oppositeComposition.apply with238      category, hInM, fgIn, innerComposable239    have assoc := Category.associative with category, fInM, gInM, hInM, fg, gh240    rw [hgValue, gfValue, leftValue, rightValue]241    symm242    exact assoc243244theorem InversePair.opposite (f g : Set)245  requires pair : InversePair(C, f, g)246  shows InversePair(opposite(C), f, g)247proof248  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair249  have gfComposable : cod(C)(g) = dom(C)(f) by cc250  have fgComposable : cod(C)(f) = dom(C)(g) by cc251  have gfValue := oppositeComposition.apply with252    category, gInM, fInM, gfComposable253  have fgValue := oppositeComposition.apply with254    category, fInM, gInM, fgComposable255  unfold InversePair256  rw [opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id]257  refine ⟨fInM, gInM, codG, domG, ?_, ?_⟩258  . rw gfValue259    exact rightLaw260  . rw fgValue261    exact leftLaw262263theorem InversePair.of_opposite (f g : Set)264  requires pair : InversePair(opposite(C), f, g)265  shows InversePair(C, f, g)266proof267  unfold InversePair at pair268  rw [opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id] at pair269  obtain ⟨fInM, gInM, codG, domG, leftLaw, rightLaw⟩ := pair270  have gfComposable : cod(C)(g) = dom(C)(f) by cc271  have fgComposable : cod(C)(f) = dom(C)(g) by cc272  have gfValue := oppositeComposition.apply with273    category, gInM, fInM, gfComposable274  have fgValue := oppositeComposition.apply with275    category, fInM, gInM, fgComposable276  rw gfValue at leftLaw277  rw fgValue at rightLaw278  unfold InversePair279  refine ⟨fInM, gInM, domG, codG, rightLaw, leftLaw⟩280281theorem Isomorphism.opposite (f : Set)282  shows Isomorphism(C, f) ↔ Isomorphism(opposite(C), f)283proof284  constructor285  . intro iso286    obtain ⟨g, pair⟩ := iso287    have opposite := InversePair.opposite with category, pair288    exact Isomorphism.of_pair with opposite289  . intro iso290    obtain ⟨g, pair⟩ := iso291    have original := InversePair.of_opposite with category, pair292    exact Isomorphism.of_pair with original293294theorem Isomorphic.opposite (a b : Set)295  shows Isomorphic(C, a, b) ↔ Isomorphic(opposite(C), b, a)296proof297  have homs := hom.opposite at C, b, a298  constructor299  . intro iso300    obtain ⟨f, fHom, fIso⟩ := iso301    have oppositeIso := Isomorphism.opposite at C, f with category302    have fIsoOpposite := oppositeIso.forward with fIso303    rw ← homs at fHom304    exact Isomorphic.of_hom with fHom, fIsoOpposite305  . intro iso306    obtain ⟨f, fHom, fIso⟩ := iso307    have oppositeIso := Isomorphism.opposite at C, f with category308    have fIsoOriginal := oppositeIso.backward with fIso309    rw homs at fHom310    exact Isomorphic.of_hom with fHom, fIsoOriginal311312-- Monomorphisms of a category are the epimorphisms of its opposite.313theorem Monomorphism.opposite (f : Set)314  shows Monomorphism(C, f) ↔ Epimorphism(opposite(C), f)315proof316  constructor317  . intro mono318    have fInM := Monomorphism.morphism with mono319    obtain ⟨objE, morE, domE, codE, compE, idE⟩ := opposite.projections at C320    unfold Epimorphism321    rw under morE322    rw under domE323    rw under codE324    rw under compE325    refine ⟨fInM, ?_⟩326    intros u uInM v vInM uComposable vComposable same327    have uValue := oppositeComposition.apply with328      category, uInM, fInM, uComposable329    have vValue := oppositeComposition.apply with330      category, vInM, fInM, vComposable331    have uReversed : dom(C)(f) = cod(C)(u) by cc332    have vReversed : dom(C)(f) = cod(C)(v) by cc333    have original : f ∘ u = f ∘ v by cc334    exact Monomorphism.cancel with335      mono, uInM, vInM, uReversed, vReversed, original336  . intro epi337    obtain ⟨objE, morE, domE, codE, compE, idE⟩ := opposite.projections at C338    unfold Epimorphism at epi339    rw under morE at epi340    rw under domE at epi341    rw under codE at epi342    rw under compE at epi343    obtain ⟨fInM, cancel⟩ := epi344    unfold Monomorphism345    refine ⟨fInM, ?_⟩346    intros u uInM v vInM uComposable vComposable same347    have uReversed : cod(C)(u) = dom(C)(f) by cc348    have vReversed : cod(C)(v) = dom(C)(f) by cc349    have uValue := oppositeComposition.apply with350      category, uInM, fInM, uReversed351    have vValue := oppositeComposition.apply with352      category, vInM, fInM, vReversed353    have opposite : oppositeComposition(C)(u, f) =354        oppositeComposition(C)(v, f) by cc355    exact cancel with u, uInM, v, vInM, uReversed, vReversed, opposite356357theorem Epimorphism.opposite (f : Set)358  shows Epimorphism(C, f) ↔ Monomorphism(opposite(C), f)359proof360  constructor361  . intro epi362    have fInM := Epimorphism.morphism with epi363    obtain ⟨objE, morE, domE, codE, compE, idE⟩ := opposite.projections at C364    unfold Monomorphism365    rw under morE366    rw under domE367    rw under codE368    rw under compE369    refine ⟨fInM, ?_⟩370    intros u uInM v vInM uComposable vComposable same371    have uValue := oppositeComposition.apply with372      category, fInM, uInM, uComposable373    have vValue := oppositeComposition.apply with374      category, fInM, vInM, vComposable375    have uReversed : dom(C)(u) = cod(C)(f) by cc376    have vReversed : dom(C)(v) = cod(C)(f) by cc377    have original : u ∘ f = v ∘ f by cc378    exact Epimorphism.cancel with379      epi, uInM, vInM, uReversed, vReversed, original380  . intro mono381    obtain ⟨objE, morE, domE, codE, compE, idE⟩ := opposite.projections at C382    unfold Monomorphism at mono383    rw under morE at mono384    rw under domE at mono385    rw under codE at mono386    rw under compE at mono387    obtain ⟨fInM, cancel⟩ := mono388    unfold Epimorphism389    refine ⟨fInM, ?_⟩390    intros u uInM v vInM uComposable vComposable same391    have uReversed : cod(C)(f) = dom(C)(u) by cc392    have vReversed : cod(C)(f) = dom(C)(v) by cc393    have uValue := oppositeComposition.apply with394      category, fInM, uInM, uReversed395    have vValue := oppositeComposition.apply with396      category, fInM, vInM, vReversed397    have opposite : oppositeComposition(C)(f, u) =398        oppositeComposition(C)(f, v) by cc399    exact cancel with u, uInM, v, vInM, uReversed, vReversed, opposite400401theorem Retraction.opposite (f r : Set)402  requires retraction : Retraction(C, f, r)403  shows SectionOf(opposite(C), f, r)404proof405  obtain ⟨fInM, rInM, domR, codR, law⟩ := retraction406  have composable : cod(C)(f) = dom(C)(r) by cc407  have value := oppositeComposition.apply with category, fInM, rInM, composable408  unfold SectionOf409  rw [opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id]410  refine ⟨fInM, rInM, codR, domR, ?_⟩411  rw value412  exact law413414theorem SectionOf.opposite (f s : Set)415  requires section : SectionOf(C, f, s)416  shows Retraction(opposite(C), f, s)417proof418  obtain ⟨fInM, sInM, domS, codS, law⟩ := section419  have composable : cod(C)(s) = dom(C)(f) by cc420  have value := oppositeComposition.apply with category, sInM, fInM, composable421  unfold Retraction422  rw [opposite.mor, opposite.dom, opposite.cod, opposite.comp, opposite.id]423  refine ⟨fInM, sInM, codS, domS, ?_⟩424  rw value425  exact law426427-- Terminal objects of a category are the initial objects of its opposite.428theorem Terminal.opposite (t : Set)429  shows Terminal(C, t) ↔ Initial(opposite(C), t)430proof431  constructor432  . intro terminal433    obtain ⟨tInO, universal⟩ := terminal434    have objE := opposite.obj at C435    unfold Initial436    rw under objE437    refine ⟨tInO, ?_⟩438    intros a aInO439    have homs := hom.opposite at C, t, a440    obtain ⟨f, fHom, unique⟩ := universal with a, aInO441    refine ⟨f, ?_, ?_⟩442    . rw homs443      exact fHom444    . intros g gHom445      rw homs at gHom446      exact unique with g, gHom447  . intro initial448    have objE := opposite.obj at C449    unfold Initial at initial450    rw under objE at initial451    obtain ⟨tInO, universal⟩ := initial452    unfold Terminal453    refine ⟨tInO, ?_⟩454    intros a aInO455    have homs := hom.opposite at C, t, a456    obtain ⟨f, fHom, unique⟩ := universal with a, aInO457    refine ⟨f, ?_, ?_⟩458    . rw ← homs459      exact fHom460    . intros g gHom461      rw ← homs at gHom462      exact unique with g, gHom463464theorem Initial.opposite (i : Set)465  shows Initial(C, i) ↔ Terminal(opposite(C), i)466proof467  constructor468  . intro initial469    obtain ⟨iInO, universal⟩ := initial470    have objE := opposite.obj at C471    unfold Terminal472    rw under objE473    refine ⟨iInO, ?_⟩474    intros a aInO475    have homs := hom.opposite at C, a, i476    obtain ⟨f, fHom, unique⟩ := universal with a, aInO477    refine ⟨f, ?_, ?_⟩478    . rw homs479      exact fHom480    . intros g gHom481      rw homs at gHom482      exact unique with g, gHom483  . intro terminal484    have objE := opposite.obj at C485    unfold Terminal at terminal486    rw under objE at terminal487    obtain ⟨iInO, universal⟩ := terminal488    unfold Initial489    refine ⟨iInO, ?_⟩490    intros a aInO491    have homs := hom.opposite at C, a, i492    obtain ⟨f, fHom, unique⟩ := universal with a, aInO493    refine ⟨f, ?_, ?_⟩494    . rw ← homs495      exact fHom496    . intros g gHom497      rw ← homs at gHom498      exact unique with g, gHom499500-- The opposite of the opposite composes as the original category.501theorem oppositeComposition.involutive502  shows oppositeComposition(opposite(C)) = comp(C)503proof504  have opposite := Category.opposite with category505  have doubleFunction := oppositeComposition.function with opposite506  have compFunction := Category.comp_function with category507  have pairs := oppositePairs.opposite at C508  rw [pairs, opposite.mor] at doubleFunction509  apply FunctionBetween.ext with doubleFunction, compFunction510  intros p member511  obtain ⟨bounded, g, gInM, f, fInM, shape, composable⟩ :=512    composablePairs.membership.forward with member513  have reversed : cod(C)(f) = dom(C)(g) by cc514  have innerValue := oppositeComposition.apply with515    category, fInM, gInM, reversed516  have gInOpposite : g ∈ mor(opposite(C))517    rw opposite.mor518    exact gInM519  have fInOpposite : f ∈ mor(opposite(C))520    rw opposite.mor521    exact fInM522  have oppositeComposable : cod(opposite(C))(g) = dom(opposite(C))(f)523    rw [opposite.cod, opposite.dom]524    exact composable525  have outerValue := oppositeComposition.apply with526    opposite, gInOpposite, fInOpposite, oppositeComposable527  rw opposite.comp at outerValue528  rw shape529  unfold call2 at outerValue530  rw outerValue531  simp [call2] at innerValue532  simp [call2, innerValue]533534end OppositeLaws535536-- A functor between categories is a functor between their opposites.537def oppositeFunctor (F : Set) : Set :=538  Functor.mk(Functor.obj(F), Functor.map(F), opposite(src(F)), opposite(tgt(F)))539540section OppositeFunctor541variable (F C D : Set)542hypothesis functor : F : C ⥤ D543544theorem oppositeFunctor.obj (a : Set)545  requires aInO : a ∈ obj(C)546  shows obj(oppositeFunctor(F))(a) = F(a)547proof548  simp [oppositeFunctor, Functor.mk.obj]549550theorem oppositeFunctor.map (f : Set)551  requires fInM : f ∈ mor(C)552  shows map(oppositeFunctor(F))(f) = F(f)553proof554  simp [oppositeFunctor, Functor.mk.map]555556theorem Functor.opposite557  shows oppositeFunctor(F) : opposite(C) ⥤ opposite(D)558proof559  have srcF := Functor.source with functor560  have tgtF := Functor.target with functor561  have source := Functor.source_category with functor562  have target := Functor.target_category with functor563  have sourceOpposite := Category.opposite with source564  have targetOpposite := Category.opposite with target565  have srcLaw : src(oppositeFunctor(F)) = opposite(C)566    simp [oppositeFunctor, Functor.mk.src, srcF]567  have tgtLaw : tgt(oppositeFunctor(F)) = opposite(D)568    simp [oppositeFunctor, Functor.mk.tgt, tgtF]569  have objC := opposite.obj at C570  have objD := opposite.obj at D571  have morC := opposite.mor at C572  have morD := opposite.mor at D573  have objects : obj(oppositeFunctor(F)) : obj(opposite(C)) → obj(opposite(D))574    have function := Functor.object_function with functor575    unfold oppositeFunctor576    rw [Functor.mk.obj, objC, objD]577    exact function578  have morphisms : map(oppositeFunctor(F)) : mor(opposite(C)) → mor(opposite(D))579    have function := Functor.morphism_function with functor580    unfold oppositeFunctor581    rw [Functor.mk.map, morC, morD]582    exact function583  have shape : Functor.Data(oppositeFunctor(F)) by simp [oppositeFunctor, Functor.mk.data]584  unfold Functor585  refine ⟨shape, sourceOpposite, targetOpposite, objects, morphisms, ?_, ?_, ?_, srcLaw, tgtLaw⟩586  . intros a aIn b bIn f fHom587    rw opposite.obj at aIn588    rw opposite.obj at bIn589    unfold Morphism at fHom590    rw [opposite.mor, opposite.dom, opposite.cod] at fHom591    obtain ⟨fInM, codF, domF⟩ := fHom592    have typed := Morphism.of_dom_cod at C, f, b, a with source, fInM, domF, codF593    have image := Functor.map_hom at F, C, D, b, a, f with bIn, aIn, typed, functor594    have objA := oppositeFunctor.obj with functor, aIn595    have objB := oppositeFunctor.obj with functor, bIn596    have mapF := oppositeFunctor.map with functor, fInM597    unfold Morphism598    rw [opposite.mor, opposite.dom, opposite.cod, objA, objB, mapF]599    obtain ⟨imageIn, domImage, codImage⟩ := image600    refine ⟨imageIn, codImage, domImage⟩601  . intros a aIn602    rw opposite.obj at aIn603    have idIn := Category.id_closed with source, aIn604    have objA := oppositeFunctor.obj with functor, aIn605    have mapId := oppositeFunctor.map with functor, idIn606    rw [opposite.id, opposite.id, mapId, objA]607    exact Functor.map_id with functor, aIn608  . intros a aIn b bIn c cIn f fHom g gHom609    rw opposite.obj at aIn610    rw opposite.obj at bIn611    rw opposite.obj at cIn612    unfold Morphism at fHom613    unfold Morphism at gHom614    rw [opposite.mor, opposite.dom, opposite.cod] at fHom615    rw [opposite.mor, opposite.dom, opposite.cod] at gHom616    obtain ⟨fInM, codF, domF⟩ := fHom617    obtain ⟨gInM, codG, domG⟩ := gHom618    have fTyped := Morphism.of_dom_cod at C, f, b, a with source, fInM, domF, codF619    have gTyped := Morphism.of_dom_cod at C, g, c, b with source, gInM, domG, codG620    have composable : cod(C)(g) = dom(C)(f) by cc621    have fImage := Functor.map_hom at F, C, D, b, a, f with bIn, aIn, fTyped, functor622    have gImage := Functor.map_hom at F, C, D, c, b, g with cIn, bIn, gTyped, functor623    have imageComposable : cod(D)(F(g)) = dom(D)(F(f)) by cc624    have gImageIn := Functor.morphism_closed with functor, gInM625    have fImageIn := Functor.morphism_closed with functor, fInM626    have sourceValue := oppositeComposition.apply with source, gInM, fInM, composable627    have targetValue := oppositeComposition.apply with target, gImageIn, fImageIn, imageComposable628    have reversed : dom(C)(f) = cod(C)(g) by cc629    have gfIn : oppositeComposition(C)(g, f) ∈ mor(C)630      rw sourceValue631      exact Category.comp_closed with source, fInM, gInM, reversed632    have mapF := oppositeFunctor.map with functor, fInM633    have mapG := oppositeFunctor.map with functor, gInM634    have mapGF := oppositeFunctor.map with functor, gfIn635    rw [opposite.comp, opposite.comp, mapGF, mapG, mapF, sourceValue, targetValue]636    exact Functor.map_comp with *637638end OppositeFunctor639