dftermo3

set.mm

@@ -202935,6 +202935,19 @@ concepts associated with those structures (product, substructure...)
       WAVPTVRTWATWEVHRKMAWEBVHXFWSVAVDAWEXGVIRKXJXGCVIXIXHVAVBABCDVEVFVG $.
   $}
 
+  ${
+    $d f u z $.
+    $( ` oppCat ` restricted to ` Cat ` is a function from ` Cat ` to ` Cat ` .
+       (Contributed by Zhi Wang, 29-Aug-2024.) $)
+    oppccatf $p |- ( oppCat |` Cat ) : Cat --> Cat $=
+      ( vc vf vu vz ccat coppc cres wf cdm wcel cfv cvv cnx chom ctpos cop csts
+      cv co cco wa wfun wral wb cbs cxp c2nd c1st df-oppc funmpt2 ffvresb ax-mp
+      cmpo elex ovex dmmpti eleqtrrdi eqid oppccat jca mprgbir ) EEFEGHZARZFIZJ
+      ZVCFKZEJZUAZAEFUBVBVHAEUCUDBLBRZMNKVINKOPQSZMTKCDVIUEKZVKUFVKDRCRZUGKPVLU
+      HKVITKSOUMPZQSZFDCBUIZUJAEEFUKULVCEJZVEVGVPVCLVDVCEUNBLVNFVJVMQUOVOUPUQVC
+      VFVFURUSUTVA $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -207308,16 +207321,17 @@ is always a subcategory (and it is full, meaning that all morphisms of
     $( An object A is said to be an initial object provided that for each
        object B there is exactly one morphism from A to B. Definition 7.1 in
        [Adamek] p. 101, or definition in [Lang] p. 57 (called "a universally
-       repelling object" there).  See ~ dfinito2 for an alternate definition
-       depending on ~ df-termo .  (Contributed by AV, 3-Apr-2020.) $)
+       repelling object" there).  See ~ dfinito2 and ~ dfinito3 for alternate
+       definitions depending on ~ df-termo .  (Contributed by AV,
+       3-Apr-2020.) $)
     df-inito $a |- InitO = ( c e. Cat |-> { a e. ( Base ` c ) |
                       A. b e. ( Base ` c ) E! h h e. ( a ( Hom ` c ) b ) } ) $.
 
     $( An object A is called a terminal object provided that for each object B
        there is exactly one morphism from B to A. Definition 7.4 in [Adamek]
        p. 102, or definition in [Lang] p. 57 (called "a universally attracting
-       object" there).  See ~ dftermo2 for an alternate definition depending on
-       ~ df-inito .  (Contributed by AV, 3-Apr-2020.) $)
+       object" there).  See ~ dftermo2 and ~ dftermo3 for alternate definitions
+       depending on ~ df-inito .  (Contributed by AV, 3-Apr-2020.) $)
     df-termo $a |- TermO = ( c e. Cat |-> { a e. ( Base ` c ) |
                       A. b e. ( Base ` c ) E! h h e. ( b ( Hom ` c ) a ) } ) $.
 
@@ -207327,6 +207341,24 @@ is always a subcategory (and it is full, meaning that all morphisms of
     df-zeroo $a |- ZeroO = ( c e. Cat
                              |-> ( ( InitO ` c ) i^i ( TermO ` c ) ) ) $.
 
+    $( ` InitO ` is a function on ` Cat ` .  (Contributed by Zhi Wang,
+       29-Aug-2024.) $)
+    initofn $p |- InitO Fn Cat $=
+      ( vc vh va vb ccat cv chom cfv co wcel weu wral crab cinito fvex df-inito
+      cbs rabex fnmpti ) AEBFCFDFAFZGHIJBKDTQHZLZCUAMNUBCUATQORBCDAPS $.
+
+    $( ` TermO ` is a function on ` Cat ` .  (Contributed by Zhi Wang,
+       29-Aug-2024.) $)
+    termofn $p |- TermO Fn Cat $=
+      ( vc vh vb va ccat cv chom cfv co wcel weu wral crab ctermo fvex df-termo
+      cbs rabex fnmpti ) AEBFCFDFAFZGHIJBKCTQHZLZDUAMNUBDUATQORBDCAPS $.
+
+    $( ` ZeroO ` is a function on ` Cat ` .  (Contributed by Zhi Wang,
+       29-Aug-2024.) $)
+    zeroofn $p |- ZeroO Fn Cat $=
+      ( vc ccat cv cinito cfv ctermo cin czeroo fvex inex1 df-zeroo fnmpti ) AB
+      ACZDEZMFEZGHNOMDIJAKL $.
+
     $( Reverse closure for an initial object:  If a class has an initial
        object, the class is a category.  (Contributed by AV, 4-Apr-2020.) $)
     initorcl $p |- ( I e. ( InitO ` C ) -> C e. Cat ) $=
@@ -207487,6 +207519,22 @@ is always a subcategory (and it is full, meaning that all morphisms of
       PIZQIZRBDCASAFVDVBUOFKZVDULUNUMVCHIZJZKZBLZCUTNZDUTOVBVEUTVCBVFDCUOVCVCTZ
       UAUTUOVCVKUTTUBVFTUCVJVADUTVIUSCUTVHURBVGUQULUOUPVCUNUMUPTVKUDUEUFUHUIUJU
       GUK $.
+
+    $( An alternate definition of ~ df-inito depending on ~ df-termo , without
+       dummy variables.  (Contributed by Zhi Wang, 29-Aug-2024.) $)
+    dfinito3 $p  |- InitO = ( TermO o. ( oppCat |` Cat ) ) $=
+      ( vc ccat cv coppc cres cfv ctermo cmpt ccom cinito fvres fveq2d mpteq2ia
+      wcel cvv wf wceq wfn termofn dffn2 mpbi oppccatf fcompt dfinito2 3eqtr4ri
+      mp2an ) ABACZDBEZFZGFZHZABUGDFZGFZHGUHIZJABUJUMUGBNUIULGUGBDKLMBOGPZBBUHP
+      UNUKQGBRUOSBGTUAUBAGUHBBOUCUFAUDUE $.
+
+    $( An alternate definition of ~ df-termo depending on ~ df-inito , without
+       dummy variables.  (Contributed by Zhi Wang, 29-Aug-2024.) $)
+    dftermo3 $p  |- TermO = ( InitO o. ( oppCat |` Cat ) ) $=
+      ( vc ccat cv coppc cres cfv cinito cmpt ccom ctermo fvres fveq2d mpteq2ia
+      wcel cvv wf wceq wfn initofn dffn2 mpbi oppccatf fcompt dftermo2 3eqtr4ri
+      mp2an ) ABACZDBEZFZGFZHZABUGDFZGFZHGUHIZJABUJUMUGBNUIULGUGBDKLMBOGPZBBUHP
+      UNUKQGBRUOSBGTUAUBAGUHBBOUCUFAUDUE $.
   $}
 
   ${