Beagle---0.9.52.THM-CRf.s

%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : ITP303_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s

% Computer : n007.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Apr  9 06:53:36 PM UTC 2025

% Result   : Theorem 33.69s 15.01s
% Output   : CNFRefutation 33.85s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : ITP303_1 : TPTP v9.0.0. Released v8.0.0.
% 0.04/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34  % Computer : n007.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Tue Apr  8 02:15:23 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 33.69/15.01  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.69/15.02  
% 33.69/15.02  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.85/15.04  %$ mapsTo$c > mapsTo$b > nt_abbrev$c > nt_abbrev$b > nt_abbrev$ > functor_abbrev$b > functor_abbrev$a > functor_abbrev$ > compDefined$c > compDefined$b > nTCompDefined$e > nTCompDefined$d > nTCompDefined$c > nTCompDefined$b > nTCompDefined$ > member$o > member$n > member$m > member$l > member$k > member$j > member$i > member$h > member$g > member$f > member$e > member$d > member$c > member$b > member$a > member$ > functor_comp_def$c > functor_comp_def$b > functor_comp_def$a > functor_comp_def$ > fun_app$q > fun_app$j > fun_app$i > fun_app$h > fun_app$g > fun_app$f > fun_app$e > fun_app$d > fun_app$c > fun_app$b > fun_app$a > preFunctor$a > natTransP$f > natTransP$e > natTransP$d > natTransP$c > natTransP$b > natTransP$ > natTransExt$ > natTrans$f > natTrans$e > natTrans$d > natTrans$c > natTrans$b > natTrans$a > lSCategory_axioms$ > lSCategory$ > functorM_axioms$ > functorM$ > functorExt$ > functor$f > functor$e > functor$d > functor$c > functor$b > functor$a > extCategory$a > extCategory$ > equivalence$ > category_axioms$b > category_axioms$a > category_axioms$ > category$b > category$a > category$ > category_ext$b > category_ext$a > category_ext$ > natTrans_ext$a > natTrans_ext$ > functor_ext$a > functor_ext$ > zFfun$ > restrict$a > restrict$ > mapsTo$a > mapsTo$ > hOMCollection$ > constFunctor$b > constFunctor$a > constFunctor$ > comp$b > zF2mor$ > yFtorNT$ > uus$ > uuq$ > uup$ > uuo$ > uun$ > uum$ > uul$ > restrict$f > restrict$e > restrict$d > restrict$c > restrict$b > pair$a > pair$ > objIso$ > nt_abbrev$a > natTransMap$f > natTransMap$e > natTransMap$c > natTransMap$b > natTransComp$g > natTransComp$f > natTransComp$e > natTransComp$d > natTransComp$b > natTransComp$a > natTransComp$ > nTDom_update$ > nTCod_update$a > nTCod_update$ > more_update$ > mapO$f > mapO$e > mapO$d > mapO$a > mapO$ > mapM$f > mapM$e > mapM$d > mapM$c > mapM$a > lSCategory_ext$ > inverse_rel$a > inverse_rel$ > inverse$a > image$ > homSet$ > homFtorMapContra$ > homFtorMap$ > homFtorContra$a > homFtorContra$ > homFtor$a > homFtor$ > functorComp$a > functorComp$ > fun_app$z > fun_app$y > fun_app$x > fun_app$w > fun_app$v > fun_app$u > fun_app$t > fun_app$s > fun_app$r > fun_app$p > fun_app$o > fun_app$n > fun_app$m > fun_app$l > fun_app$k > fun_app$af > fun_app$ae > fun_app$ad > fun_app$ac > fun_app$ab > fun_app$aa > fun_app$ > dom$b > compDefined$a > compDefined$ > comp$c > cod$b > catExp$c > catExp$b > catExp$a > catExp$ > #nlpp > yFtorNT$a > yFtor$ > uuz$ > uuy$ > uux$ > uuw$ > uur$ > uuk$ > uuj$ > uui$ > uuh$ > uug$ > uuf$ > uue$ > uud$ > uuc$ > uub$ > uua$ > uu$ > unitFunctor$ > the$a > the$ > oppositeCategory$c > oppositeCategory$a > obj_update$ > obj$a > obj$ > natTransMap$d > natTransMap$a > natTransMap$ > nTDom$f > nTDom$e > nTDom$d > nTDom$c > nTDom$b > nTDom$a > nTCompDefined$a > nTCod$f > nTCod$e > nTCod$d > nTCod$c > nTCod$b > nTCod$a > nTCatDom$f > nTCatDom$e > nTCatDom$d > nTCatDom$c > nTCatDom$b > nTCatDom$a > nTCatDom$ > nTCatCod$f > nTCatCod$e > nTCatCod$d > nTCatCod$c > nTCatCod$b > nTCatCod$a > nTCatCod$ > more_update$a > more$e > more$d > more$c > more$b > more$a > more$ > mor_update$a > mor_update$ > mor2ZF$ > mor$c > mor$b > mor$a > mor$ > mapO$c > mapO$b > mapM$b > mapM$ > makeNT$a > makeNT$ > makeCat$c > makeCat$b > isomorphism$a > isomorphism$ > inverse$ > identityFunctor$a > identityFunctor$ > id_update$ > idNatTrans$e > idNatTrans$c > idNatTrans$b > idNatTrans$a > idNatTrans$ > id$a > id$ > extensional$f > extensional$e > extensional$d > extensional$c > extensional$b > extensional$a > extensional$ > elem$ > dom_update$ > dom$a > dom$ > comp_update$ > comp$d > comp$a > comp$ > collect$j > collect$i > collect$h > collect$g > collect$f > collect$e > collect$d > collect$c > collect$b > collect$a > collect$ > cod_update$ > cod$a > cod$ > catDom_update$a > catDom_update$ > catDom$f > catDom$e > catDom$d > catDom$c > catDom$b > catDom$a > catDom$ > catCod$f > catCod$e > catCod$d > catCod$c > catCod$b > catCod$a > catCod$ > case_prod$a > case_prod$ > zFfunDom$ > zFfunComp$ > zFfunCod$ > zFfunApp$ > uuv$ > uuu$ > uut$ > unity$ > top$ > set$a > set$ > preFunctor$ > oppositeCategory$b > oppositeCategory$ > natTransP$a > natTransExt$a > natTransComp$c > natTrans$ > nTDom$ > nTCod$ > makeFtor$ > makeCat$a > makeCat$ > isZFfun$ > idNatTrans$d > functorM_axioms$a > functorM$a > functorExt$a > functor$ > f$ > explode$ > equivalence_axioms$ > equivalence$a > c$ > #skF_21 > #skF_60 > #skF_137 > #skF_69 > #skF_6 > #skF_180 > #skF_23 > #skF_170 > #skF_15 > #skF_97 > #skF_214 > #skF_52 > #skF_36 > #skF_90 > #skF_192 > #skF_33 > #skF_209 > #skF_153 > #skF_59 > #skF_40 > #skF_184 > #skF_64 > #skF_47 > #skF_80 > #skF_42 > #skF_11 > #skF_152 > #skF_76 > #skF_227 > #skF_75 > #skF_162 > #skF_177 > #skF_142 > #skF_163 > #skF_143 > #skF_222 > #skF_195 > #skF_1 > #skF_74 > #skF_200 > #skF_22 > #skF_2 > #skF_149 > #skF_121 > #skF_127 > #skF_191 > #skF_205 > #skF_140 > #skF_32 > #skF_41 > #skF_126 > #skF_202 > #skF_34 > #skF_82 > #skF_57 > #skF_160 > #skF_92 > #skF_199 > #skF_8 > #skF_78 > #skF_157 > #skF_109 > #skF_88 > #skF_155 > #skF_27 > #skF_178 > #skF_197 > #skF_77 > #skF_226 > #skF_46 > #skF_4 > #skF_102 > #skF_212 > #skF_150 > #skF_223 > #skF_128 > #skF_73 > #skF_101 > #skF_179 > #skF_203 > #skF_194 > #skF_38 > #skF_207 > #skF_45 > #skF_154 > #skF_147 > #skF_133 > #skF_30 > #skF_198 > #skF_216 > #skF_93 > #skF_72 > #skF_123 > #skF_218 > #skF_217 > #skF_158 > #skF_166 > #skF_139 > #skF_130 > #skF_50 > #skF_56 > #skF_5 > #skF_95 > #skF_221 > #skF_113 > #skF_54 > #skF_44 > #skF_116 > #skF_86 > #skF_106 > #skF_99 > #skF_87 > #skF_3 > #skF_206 > #skF_164 > #skF_172 > #skF_146 > #skF_94 > #skF_10 > #skF_26 > #skF_65 > #skF_35 > #skF_111 > #skF_107 > #skF_100 > #skF_84 > #skF_49 > #skF_215 > #skF_183 > #skF_19 > #skF_131 > #skF_105 > #skF_96 > #skF_196 > #skF_189 > #skF_182 > #skF_91 > #skF_181 > #skF_119 > #skF_48 > #skF_144 > #skF_20 > #skF_12 > #skF_16 > #skF_108 > #skF_173 > #skF_66 > #skF_204 > #skF_70 > #skF_28 > #skF_89 > #skF_71 > #skF_225 > #skF_29 > #skF_115 > #skF_167 > #skF_148 > #skF_187 > #skF_201 > #skF_156 > #skF_120 > #skF_186 > #skF_124 > #skF_31 > #skF_171 > #skF_85 > #skF_112 > #skF_13 > #skF_51 > #skF_145 > #skF_224 > #skF_135 > #skF_176 > #skF_18 > #skF_81 > #skF_136 > #skF_39 > #skF_25 > #skF_151 > #skF_61 > #skF_208 > #skF_53 > #skF_68 > #skF_188 > #skF_141 > #skF_104 > #skF_138 > #skF_193 > #skF_83 > #skF_129 > #skF_220 > #skF_125 > #skF_110 > #skF_118 > #skF_103 > #skF_24 > #skF_55 > #skF_14 > #skF_58 > #skF_228 > #skF_17 > #skF_175 > #skF_62 > #skF_185 > #skF_98 > #skF_37 > #skF_190 > #skF_7 > #skF_67 > #skF_114 > #skF_43 > #skF_132 > #skF_219 > #skF_159 > #skF_63 > #skF_169 > #skF_213 > #skF_168 > #skF_174 > #skF_210 > #skF_9 > #skF_122 > #skF_134 > #skF_211 > #skF_79 > #skF_117 > #skF_165 > #skF_161
% 33.85/15.04  
% 33.85/15.04  %Foreground sorts:
% 33.85/15.04  tff(B_ZF_fun_bool_fun$, type, B_ZF_fun_bool_fun$: $tType ).
% 33.85/15.04  tff(A$, type, A$: $tType ).
% 33.85/15.04  tff(ZF_ZF_fun$, type, ZF_ZF_fun$: $tType ).
% 33.85/15.04  tff(ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$, type, ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_prod_ZF_fun_set$, type, ZF_ZF_prod_ZF_fun_set$: $tType ).
% 33.85/15.04  tff(A_set$, type, A_set$: $tType ).
% 33.85/15.04  tff(A_ZF_fun_set$, type, A_ZF_fun_set$: $tType ).
% 33.85/15.04  tff(A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$, type, A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(B$, type, B$: $tType ).
% 33.85/15.04  tff(B_b_prod_b_fun_set$, type, B_b_prod_b_fun_set$: $tType ).
% 33.85/15.04  tff(ZF_bool_fun$, type, ZF_bool_fun$: $tType ).
% 33.85/15.04  tff(A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$, type, A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$: $tType ).
% 33.85/15.04  tff(B_a_fun_bool_fun$, type, B_a_fun_bool_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(Unit_set$, type, Unit_set$: $tType ).
% 33.85/15.04  tff(B_ZF_fun$, type, B_ZF_fun$: $tType ).
% 33.85/15.04  tff(B_b_prod_bool_fun$, type, B_b_prod_bool_fun$: $tType ).
% 33.85/15.04  tff(B_b_b_fun_fun$, type, B_b_b_fun_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$: $tType ).
% 33.85/15.04  tff(A_bool_fun$, type, A_bool_fun$: $tType ).
% 33.85/15.04  tff(C$, type, C$: $tType ).
% 33.85/15.04  tff(ZF_set_ZF_set_fun$, type, ZF_set_ZF_set_fun$: $tType ).
% 33.85/15.04  tff(B_bool_fun$, type, B_bool_fun$: $tType ).
% 33.85/15.04  tff(Unit_unit_unit_Category_ext$, type, Unit_unit_unit_Category_ext$: $tType ).
% 33.85/15.04  tff(A_b_fun$, type, A_b_fun$: $tType ).
% 33.85/15.04  tff(B_b_prod$, type, B_b_prod$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$, type, ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(A_b_b_c_LSCategory_ext_Category_ext$, type, A_b_b_c_LSCategory_ext_Category_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_fun_set$, type, ZF_ZF_fun_set$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$, type, ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_prod_ZF_fun$, type, ZF_ZF_prod_ZF_fun$: $tType ).
% 33.85/15.04  tff(A_b_fun_set$, type, A_b_fun_set$: $tType ).
% 33.85/15.04  tff(ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$, type, ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(B_b_prod_set$, type, B_b_prod_set$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$, type, ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_fun_ZF_ZF_fun_fun$, type, ZF_ZF_fun_ZF_ZF_fun_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_set_fun$, type, ZF_ZF_set_fun$: $tType ).
% 33.85/15.04  tff(A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$, type, A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$: $tType ).
% 33.85/15.04  tff(ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$, type, ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(B_set$, type, B_set$: $tType ).
% 33.85/15.04  tff(A_ZF_fun_bool_fun$, type, A_ZF_fun_bool_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(Unit_unit_fun$, type, Unit_unit_fun$: $tType ).
% 33.85/15.04  tff(ZF$, type, ZF$: $tType ).
% 33.85/15.04  tff(A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$, type, A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$, type, A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_prod$, type, ZF_ZF_prod$: $tType ).
% 33.85/15.04  tff(ZF_ZF_unit_Category_ext$, type, ZF_ZF_unit_Category_ext$: $tType ).
% 33.85/15.04  tff(A_ZF_fun$, type, A_ZF_fun$: $tType ).
% 33.85/15.04  tff(ZF_set$, type, ZF_set$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$: $tType ).
% 33.85/15.04  tff(B_ZF_fun_set$, type, B_ZF_fun_set$: $tType ).
% 33.85/15.04  tff(B_b_fun$, type, B_b_fun$: $tType ).
% 33.85/15.04  tff(A_b_fun_bool_fun$, type, A_b_fun_bool_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_prod_set$, type, ZF_ZF_prod_set$: $tType ).
% 33.85/15.04  tff(B_a_fun$, type, B_a_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$, type, ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$: $tType ).
% 33.85/15.04  tff(B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$, type, B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$: $tType ).
% 33.85/15.04  tff(B_c_LSCategory_ext$, type, B_c_LSCategory_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$, type, ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$: $tType ).
% 33.85/15.04  tff(B_a_fun_set$, type, B_a_fun_set$: $tType ).
% 33.85/15.04  tff(A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$, type, A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$, type, ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_fun_fun$, type, ZF_ZF_ZF_fun_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$, type, ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$: $tType ).
% 33.85/15.04  tff(Unit$, type, Unit$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$: $tType ).
% 33.85/15.04  tff(ZF_set_set$, type, ZF_set_set$: $tType ).
% 33.85/15.04  tff(B_b_prod_b_fun$, type, B_b_prod_b_fun$: $tType ).
% 33.85/15.04  tff(B_set_b_set_fun$, type, B_set_b_set_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_prod_bool_fun$, type, ZF_ZF_prod_bool_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$, type, ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$: $tType ).
% 33.85/15.04  tff(A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$, type, A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$: $tType ).
% 33.85/15.04  tff(ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$, type, ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$: $tType ).
% 33.85/15.04  
% 33.85/15.04  %Background operators:
% 33.85/15.04  
% 33.85/15.04  
% 33.85/15.04  %Foreground operators:
% 33.85/15.04  tff(natTransP$c, type, natTransP$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(homFtorContra$a, type, homFtorContra$a: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(more$, type, more$: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > Unit$).
% 33.85/15.04  tff(nTCatCod$f, type, nTCatCod$f: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > Unit_unit_unit_Category_ext$).
% 33.85/15.04  tff(member$m, type, member$m: (ZF_ZF_prod_ZF_fun$ * ZF_ZF_prod_ZF_fun_set$) > $o).
% 33.85/15.04  tff('#skF_21', type, '#skF_21': (B_b_prod_bool_fun$ * B_b_prod_bool_fun$) > B_b_prod$).
% 33.85/15.04  tff('#skF_60', type, '#skF_60': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(idNatTrans$a, type, idNatTrans$a: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_137', type, '#skF_137': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_69', type, '#skF_69': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(natTransP$a, type, natTransP$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$).
% 33.85/15.04  tff('#skF_6', type, '#skF_6': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_180', type, '#skF_180': ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff(pair$, type, pair$: (ZF$ * ZF$) > ZF_ZF_prod$).
% 33.85/15.04  tff('#skF_23', type, '#skF_23': (ZF_bool_fun$ * ZF_bool_fun$) > ZF$).
% 33.85/15.04  tff(inverse_rel$a, type, inverse_rel$a: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > B_bool_fun$).
% 33.85/15.04  tff('#skF_170', type, '#skF_170': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(catDom$c, type, catDom$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff('#skF_15', type, '#skF_15': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(extensional$, type, extensional$: ZF_set$ > ZF_ZF_fun_set$).
% 33.85/15.04  tff('#skF_97', type, '#skF_97': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(fun_app$ac, type, fun_app$ac: (ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff(makeFtor$, type, makeFtor$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$).
% 33.85/15.04  tff(cod$, type, cod$: ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_214', type, '#skF_214': (ZF_ZF_unit_Category_ext$ * ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$ * ZF_ZF_ZF_fun_fun$) > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(functorM$a, type, functorM$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(nt_abbrev$b, type, nt_abbrev$b: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ * ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ * ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$) > $o).
% 33.85/15.04  tff('#skF_52', type, '#skF_52': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_36', type, '#skF_36': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(fun_app$h, type, fun_app$h: (A_b_fun_bool_fun$ * A_b_fun$) > $o).
% 33.85/15.04  tff('#skF_90', type, '#skF_90': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_192', type, '#skF_192': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$) > ZF$).
% 33.85/15.04  tff(fun_app$r, type, fun_app$r: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(isomorphism$, type, isomorphism$: A_b_b_c_LSCategory_ext_Category_ext$ > B_bool_fun$).
% 33.85/15.04  tff('#skF_33', type, '#skF_33': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_fun$).
% 33.85/15.04  tff(member$h, type, member$h: (B$ * B_set$) > $o).
% 33.85/15.04  tff('#skF_209', type, '#skF_209': (B_set_b_set_fun$ * A_b_b_c_LSCategory_ext_Category_ext$ * B_set$ * A_b_b_c_LSCategory_ext_Category_ext$ * B_set_b_set_fun$) > B_set$).
% 33.85/15.04  tff(obj_update$, type, obj_update$: ZF_set_ZF_set_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(nTCod$f, type, nTCod$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_153', type, '#skF_153': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(collect$a, type, collect$a: B_b_prod_bool_fun$ > B_b_prod_set$).
% 33.85/15.04  tff(uuj$, type, uuj$: A_b_b_c_LSCategory_ext_Category_ext$ > B_b_b_fun_fun$).
% 33.85/15.04  tff('#skF_59', type, '#skF_59': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(dom$b, type, dom$b: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_40', type, '#skF_40': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_184', type, '#skF_184': ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(identityFunctor$, type, identityFunctor$: ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_64', type, '#skF_64': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(collect$g, type, collect$g: A_ZF_fun_bool_fun$ > A_ZF_fun_set$).
% 33.85/15.04  tff(functor_comp_def$b, type, functor_comp_def$b: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff(catCod$d, type, catCod$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff('#skF_47', type, '#skF_47': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_80', type, '#skF_80': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(fun_app$f, type, fun_app$f: (B_a_fun_bool_fun$ * B_a_fun$) > $o).
% 33.85/15.04  tff('#skF_42', type, '#skF_42': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(collect$d, type, collect$d: A_bool_fun$ > A_set$).
% 33.85/15.04  tff('#skF_11', type, '#skF_11': (ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$) > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(uuu$, type, uuu$: ZF_ZF_fun$).
% 33.85/15.04  tff(zFfunDom$, type, zFfunDom$: ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_152', type, '#skF_152': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_76', type, '#skF_76': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(functor$d, type, functor$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(collect$f, type, collect$f: B_a_fun_bool_fun$ > B_a_fun_set$).
% 33.85/15.04  tff(functor_comp_def$a, type, functor_comp_def$a: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff(natTransP$e, type, natTransP$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(nTCatDom$b, type, nTCatDom$b: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(lSCategory$, type, lSCategory$: A_b_b_c_LSCategory_ext_Category_ext$ > $o).
% 33.85/15.04  tff(nTCompDefined$e, type, nTCompDefined$e: (A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(fun_app$aa, type, fun_app$aa: (Unit_unit_fun$ * Unit$) > Unit$).
% 33.85/15.04  tff('#skF_227', type, '#skF_227': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_75', type, '#skF_75': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_162', type, '#skF_162': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff(functorExt$, type, functorExt$: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff('#skF_177', type, '#skF_177': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(uul$, type, uul$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > B_ZF_fun$).
% 33.85/15.04  tff(fun_app$v, type, fun_app$v: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(makeNT$, type, makeNT$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(natTrans_ext$, type, natTrans_ext$: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_fun$ * Unit$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_142', type, '#skF_142': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(nTCatCod$a, type, nTCatCod$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(member$k, type, member$k: (Unit$ * Unit_set$) > $o).
% 33.85/15.04  tff('#skF_163', type, '#skF_163': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_143', type, '#skF_143': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_222', type, '#skF_222': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_195', type, '#skF_195': ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff('#skF_1', type, '#skF_1': (ZF_ZF_unit_Category_ext$ * ZF_ZF_prod$) > ZF$).
% 33.85/15.04  tff(extensional$f, type, extensional$f: B_b_prod_set$ > B_b_prod_b_fun_set$).
% 33.85/15.04  tff('#skF_74', type, '#skF_74': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(fun_app$k, type, fun_app$k: (ZF_ZF_ZF_fun_fun$ * ZF$) > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_200', type, '#skF_200': ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(nTDom$a, type, nTDom$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(uut$, type, uut$: ZF_bool_fun$).
% 33.85/15.04  tff('#skF_22', type, '#skF_22': (B_b_prod_bool_fun$ * B_b_prod_bool_fun$) > B_b_prod$).
% 33.85/15.04  tff('#skF_2', type, '#skF_2': (ZF_ZF_unit_Category_ext$ * ZF_ZF_prod$) > ZF$).
% 33.85/15.04  tff('#skF_149', type, '#skF_149': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(cod$a, type, cod$a: A_b_b_c_LSCategory_ext_Category_ext$ > B_a_fun$).
% 33.85/15.04  tff(c$, type, c$: A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(comp$b, type, comp$b: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_121', type, '#skF_121': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(nTCatCod$e, type, nTCatCod$e: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(fun_app$af, type, fun_app$af: (ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$ * ZF_ZF_ZF_fun_fun$) > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff('#skF_127', type, '#skF_127': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(fun_app$u, type, fun_app$u: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(mor$b, type, mor$b: ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff('#skF_191', type, '#skF_191': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(fun_app$n, type, fun_app$n: (A_ZF_fun$ * A$) > ZF$).
% 33.85/15.04  tff(uur$, type, uur$: ZF$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(catCod$, type, catCod$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(mapO$d, type, mapO$d: (ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ * ZF$) > Unit$).
% 33.85/15.04  tff('#skF_205', type, '#skF_205': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(natTransComp$c, type, natTransComp$c: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$).
% 33.85/15.04  tff(functor$b, type, functor$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(idNatTrans$, type, idNatTrans$: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ > ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(yFtorNT$a, type, yFtorNT$a: A_b_b_c_LSCategory_ext_Category_ext$ > B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$).
% 33.85/15.04  tff('#skF_140', type, '#skF_140': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(catExp$b, type, catExp$b: (ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(functor_ext$, type, functor_ext$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$ * B_ZF_fun$ * Unit$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_32', type, '#skF_32': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_41', type, '#skF_41': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_126', type, '#skF_126': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$) > ZF$).
% 33.85/15.04  tff(fun_app$j, type, fun_app$j: (A_bool_fun$ * A$) > $o).
% 33.85/15.04  tff('#skF_202', type, '#skF_202': (ZF$ * ZF_ZF_fun$ * ZF$) > ZF$).
% 33.85/15.04  tff('#skF_34', type, '#skF_34': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > Unit$).
% 33.85/15.04  tff(natTransComp$f, type, natTransComp$f: (ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(catExp$, type, catExp$: (ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff('#skF_82', type, '#skF_82': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(functorComp$a, type, functorComp$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_57', type, '#skF_57': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(uuo$, type, uuo$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$).
% 33.85/15.04  tff('#skF_160', type, '#skF_160': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_92', type, '#skF_92': (Unit_unit_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * Unit$ * Unit_unit_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > Unit$).
% 33.85/15.04  tff(natTransMap$b, type, natTransMap$b: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ * ZF$) > B$).
% 33.85/15.04  tff(functor_abbrev$b, type, functor_abbrev$b: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$) > $o).
% 33.85/15.04  tff('#skF_199', type, '#skF_199': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(member$e, type, member$e: (B_a_fun$ * B_a_fun_set$) > $o).
% 33.85/15.04  tff(f$, type, f$: B$).
% 33.85/15.04  tff('#skF_8', type, '#skF_8': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_78', type, '#skF_78': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(homFtor$a, type, homFtor$a: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(natTrans$c, type, natTrans$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(fun_app$d, type, fun_app$d: (ZF_bool_fun$ * ZF$) > $o).
% 33.85/15.04  tff('#skF_157', type, '#skF_157': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_109', type, '#skF_109': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_88', type, '#skF_88': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_155', type, '#skF_155': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_27', type, '#skF_27': (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF$).
% 33.85/15.04  tff(dom$a, type, dom$a: ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(category_axioms$a, type, category_axioms$a: ZF_ZF_unit_Category_ext$ > $o).
% 33.85/15.04  tff(preFunctor$, type, preFunctor$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff('#skF_178', type, '#skF_178': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_197', type, '#skF_197': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_77', type, '#skF_77': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_226', type, '#skF_226': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_46', type, '#skF_46': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(natTransMap$f, type, natTransMap$f: (ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ * ZF$) > Unit$).
% 33.85/15.04  tff('#skF_4', type, '#skF_4': (A_b_b_c_LSCategory_ext_Category_ext$ * B_b_prod$) > B$).
% 33.85/15.04  tff(uup$, type, uup$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_fun$).
% 33.85/15.04  tff(mor2ZF$, type, mor2ZF$: A_b_b_c_LSCategory_ext_Category_ext$ > B_ZF_fun$).
% 33.85/15.04  tff(collect$j, type, collect$j: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$).
% 33.85/15.04  tff(nTDom$f, type, nTDom$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_102', type, '#skF_102': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(zFfunComp$, type, zFfunComp$: ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff('#skF_212', type, '#skF_212': (ZF_set_ZF_set_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_set$ * ZF_set_ZF_set_fun$) > ZF_set$).
% 33.85/15.04  tff('#skF_150', type, '#skF_150': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_223', type, '#skF_223': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_128', type, '#skF_128': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(natTrans$e, type, natTrans$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(category_ext$, type, category_ext$: (A_set$ * B_set$ * B_a_fun$ * B_a_fun$ * A_b_fun$ * B_b_b_fun_fun$ * B_c_LSCategory_ext$) > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff('#skF_73', type, '#skF_73': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff(extensional$c, type, extensional$c: B_set$ > B_a_fun_set$).
% 33.85/15.04  tff(extensional$e, type, extensional$e: A_set$ > A_b_fun_set$).
% 33.85/15.04  tff('#skF_101', type, '#skF_101': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff('#skF_179', type, '#skF_179': ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff(makeCat$b, type, makeCat$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(natTransMap$, type, natTransMap$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_fun$).
% 33.85/15.04  tff(case_prod$, type, case_prod$: ZF_ZF_ZF_fun_fun$ > ZF_ZF_prod_ZF_fun$).
% 33.85/15.04  tff(restrict$e, type, restrict$e: (A_b_fun$ * A_set$) > A_b_fun$).
% 33.85/15.04  tff('#skF_203', type, '#skF_203': (ZF$ * ZF$) > ZF$).
% 33.85/15.04  tff('#skF_194', type, '#skF_194': (ZF_ZF_unit_Category_ext$ * ZF$ * ZF$) > ZF$).
% 33.85/15.04  tff(nt_abbrev$, type, nt_abbrev$: (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff('#skF_38', type, '#skF_38': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(catCod$b, type, catCod$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(makeCat$, type, makeCat$: ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(equivalence$, type, equivalence$: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff('#skF_207', type, '#skF_207': (ZF_set_ZF_set_fun$ * ZF_ZF_unit_Category_ext$ * ZF_set$ * ZF_ZF_unit_Category_ext$ * ZF_set_ZF_set_fun$) > ZF_set$).
% 33.85/15.04  tff(natTrans_ext$a, type, natTrans_ext$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_fun$ * Unit$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(mapO$b, type, mapO$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_45', type, '#skF_45': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff('#skF_154', type, '#skF_154': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(more$b, type, more$b: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > Unit$).
% 33.85/15.04  tff(member$d, type, member$d: (B_ZF_fun$ * B_ZF_fun_set$) > $o).
% 33.85/15.04  tff(restrict$c, type, restrict$c: (A_ZF_fun$ * A_set$) > A_ZF_fun$).
% 33.85/15.04  tff(functor$c, type, functor$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ > $o).
% 33.85/15.04  tff('#skF_147', type, '#skF_147': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(makeCat$a, type, makeCat$a: A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$).
% 33.85/15.04  tff('#skF_133', type, '#skF_133': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(collect$, type, collect$: ZF_ZF_prod_bool_fun$ > ZF_ZF_prod_set$).
% 33.85/15.04  tff('#skF_30', type, '#skF_30': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A$).
% 33.85/15.04  tff('#skF_198', type, '#skF_198': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_216', type, '#skF_216': (ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_93', type, '#skF_93': (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF$ * ZF$ * ZF$) > ZF$).
% 33.85/15.04  tff(mapsTo$a, type, mapsTo$a: (ZF_ZF_unit_Category_ext$ * ZF$ * ZF$) > ZF_bool_fun$).
% 33.85/15.04  tff(set$, type, set$: ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(mapO$f, type, mapO$f: (A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(nTDom$d, type, nTDom$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$).
% 33.85/15.04  tff(fun_app$g, type, fun_app$g: (A_ZF_fun_bool_fun$ * A_ZF_fun$) > $o).
% 33.85/15.04  tff('#skF_72', type, '#skF_72': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_123', type, '#skF_123': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_218', type, '#skF_218': (ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun$ * ZF_ZF_fun_ZF_ZF_fun_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff(fun_app$e, type, fun_app$e: (B_ZF_fun_bool_fun$ * B_ZF_fun$) > $o).
% 33.85/15.04  tff(uub$, type, uub$: A_set$ > A_bool_fun$).
% 33.85/15.04  tff('#skF_217', type, '#skF_217': (ZF_ZF_fun$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun_ZF_ZF_fun_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff(uuv$, type, uuv$: ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_158', type, '#skF_158': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(yFtorNT$, type, yFtorNT$: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(comp$a, type, comp$a: A_b_b_c_LSCategory_ext_Category_ext$ > B_b_b_fun_fun$).
% 33.85/15.04  tff(uus$, type, uus$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF$) > B_bool_fun$).
% 33.85/15.04  tff(yFtor$, type, yFtor$: A_b_b_c_LSCategory_ext_Category_ext$ > A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(equivalence$a, type, equivalence$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff('#skF_166', type, '#skF_166': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(natTransComp$b, type, natTransComp$b: (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_139', type, '#skF_139': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff(uuz$, type, uuz$: ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff('#skF_130', type, '#skF_130': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_50', type, '#skF_50': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(catCod$a, type, catCod$a: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ > Unit_unit_unit_Category_ext$).
% 33.85/15.04  tff(mapsTo$b, type, mapsTo$b: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff('#skF_56', type, '#skF_56': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_5', type, '#skF_5': (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(collect$b, type, collect$b: B_bool_fun$ > B_set$).
% 33.85/15.04  tff('#skF_95', type, '#skF_95': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff('#skF_221', type, '#skF_221': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(nTDom$, type, nTDom$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$).
% 33.85/15.04  tff('#skF_113', type, '#skF_113': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_54', type, '#skF_54': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(more$a, type, more$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > Unit$).
% 33.85/15.04  tff('#skF_44', type, '#skF_44': A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(natTransP$f, type, natTransP$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_116', type, '#skF_116': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$ * A$ * ZF$) > B$).
% 33.85/15.04  tff('#skF_86', type, '#skF_86': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(catDom$b, type, catDom$b: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(catDom$d, type, catDom$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(nTCatDom$e, type, nTCatDom$e: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(nTDom_update$, type, nTDom_update$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_106', type, '#skF_106': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(id$a, type, id$a: ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_99', type, '#skF_99': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_87', type, '#skF_87': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(zF2mor$, type, zF2mor$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF$) > B$).
% 33.85/15.04  tff(member$j, type, member$j: (ZF_ZF_fun$ * ZF_ZF_fun_set$) > $o).
% 33.85/15.04  tff('#skF_3', type, '#skF_3': (A_b_b_c_LSCategory_ext_Category_ext$ * B_b_prod$) > B$).
% 33.85/15.04  tff(catDom_update$a, type, catDom_update$a: A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$).
% 33.85/15.04  tff('#skF_206', type, '#skF_206': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(fun_app$o, type, fun_app$o: (B_ZF_fun$ * B$) > ZF$).
% 33.85/15.04  tff(natTrans$d, type, natTrans$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(homSet$, type, homSet$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > A_ZF_fun$).
% 33.85/15.04  tff(functor_comp_def$, type, functor_comp_def$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff(category_ext$b, type, category_ext$b: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$ * Unit$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff('#skF_164', type, '#skF_164': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(lSCategory_axioms$, type, lSCategory_axioms$: A_b_b_c_LSCategory_ext_Category_ext$ > $o).
% 33.85/15.04  tff(natTransMap$e, type, natTransMap$e: (A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(uuf$, type, uuf$: A_b_fun_set$ > A_b_fun_bool_fun$).
% 33.85/15.04  tff('#skF_172', type, '#skF_172': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_146', type, '#skF_146': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(nTCatCod$, type, nTCatCod$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(collect$i, type, collect$i: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$).
% 33.85/15.04  tff('#skF_94', type, '#skF_94': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$ * A$ * ZF$) > B$).
% 33.85/15.04  tff(fun_app$s, type, fun_app$s: (A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ * A_b_b_c_LSCategory_ext_Category_ext$) > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff('#skF_10', type, '#skF_10': (A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ * A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ * A_b_b_c_LSCategory_ext_Category_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(extCategory$, type, extCategory$: A_b_b_c_LSCategory_ext_Category_ext$ > $o).
% 33.85/15.04  tff('#skF_26', type, '#skF_26': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A$).
% 33.85/15.04  tff('#skF_65', type, '#skF_65': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_35', type, '#skF_35': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * Unit$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * Unit_unit_fun$ * Unit_unit_fun$) > Unit$).
% 33.85/15.04  tff(constFunctor$b, type, constFunctor$b: (ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_111', type, '#skF_111': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(id$, type, id$: A_b_b_c_LSCategory_ext_Category_ext$ > A_b_fun$).
% 33.85/15.04  tff(makeNT$a, type, makeNT$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_107', type, '#skF_107': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF$) > A$).
% 33.85/15.04  tff(uuc$, type, uuc$: B_ZF_fun_set$ > B_ZF_fun_bool_fun$).
% 33.85/15.04  tff(fun_app$p, type, fun_app$p: (A_b_fun$ * A$) > B$).
% 33.85/15.04  tff('#skF_100', type, '#skF_100': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(zFfunCod$, type, zFfunCod$: ZF_ZF_fun$).
% 33.85/15.04  tff(zFfun$, type, zFfun$: (ZF$ * ZF$ * ZF_ZF_fun$) > ZF$).
% 33.85/15.04  tff('#skF_84', type, '#skF_84': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_49', type, '#skF_49': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(restrict$a, type, restrict$a: (B_b_prod_b_fun$ * B_b_prod_set$ * B_b_prod$) > B$).
% 33.85/15.04  tff(catDom$e, type, catDom$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(natTransExt$a, type, natTransExt$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$).
% 33.85/15.04  tff('#skF_215', type, '#skF_215': (ZF_ZF_unit_Category_ext$ * ZF_ZF_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun_ZF_ZF_fun_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff(lSCategory_ext$, type, lSCategory_ext$: (B_ZF_fun$ * C$) > B_c_LSCategory_ext$).
% 33.85/15.04  tff('#skF_183', type, '#skF_183': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_19', type, '#skF_19': (ZF_ZF_prod_bool_fun$ * ZF_ZF_prod_bool_fun$) > ZF_ZF_prod$).
% 33.85/15.04  tff(nTCompDefined$c, type, nTCompDefined$c: (ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(catDom$a, type, catDom$a: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(collect$e, type, collect$e: B_ZF_fun_bool_fun$ > B_ZF_fun_set$).
% 33.85/15.04  tff('#skF_131', type, '#skF_131': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(fun_app$w, type, fun_app$w: (ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$ * ZF_ZF_unit_Category_ext$) > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(nTCatCod$b, type, nTCatCod$b: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(comp$c, type, comp$c: (Unit_unit_unit_Category_ext$ * Unit$) > Unit_unit_fun$).
% 33.85/15.04  tff('#skF_105', type, '#skF_105': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_96', type, '#skF_96': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(nTCatDom$, type, nTCatDom$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(natTransComp$g, type, natTransComp$g: (A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_196', type, '#skF_196': ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff(dom_update$, type, dom_update$: ZF_ZF_fun_ZF_ZF_fun_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(category_axioms$b, type, category_axioms$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ > $o).
% 33.85/15.04  tff('#skF_189', type, '#skF_189': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff('#skF_182', type, '#skF_182': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(functor$, type, functor$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(mapO$, type, mapO$: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ * ZF$) > A$).
% 33.85/15.04  tff(natTransComp$e, type, natTransComp$e: (A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ * A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$) > A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$).
% 33.85/15.04  tff(natTrans$a, type, natTrans$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(obj$, type, obj$: ZF_ZF_unit_Category_ext$ > ZF_set$).
% 33.85/15.04  tff('#skF_91', type, '#skF_91': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(idNatTrans$b, type, idNatTrans$b: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_181', type, '#skF_181': ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(fun_app$ad, type, fun_app$ad: (ZF_set_ZF_set_fun$ * ZF_set$) > ZF_set$).
% 33.85/15.04  tff(restrict$d, type, restrict$d: (B_a_fun$ * B_set$) > B_a_fun$).
% 33.85/15.04  tff(member$o, type, member$o: (ZF_set$ * ZF_set_set$) > $o).
% 33.85/15.04  tff(comp$, type, comp$: ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(fun_app$i, type, fun_app$i: (B_bool_fun$ * B$) > $o).
% 33.85/15.04  tff(mapO$c, type, mapO$c: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A_ZF_fun$).
% 33.85/15.04  tff('#skF_119', type, '#skF_119': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_48', type, '#skF_48': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(fun_app$b, type, fun_app$b: (ZF_ZF_prod_bool_fun$ * ZF_ZF_prod$) > $o).
% 33.85/15.04  tff(natTransMap$a, type, natTransMap$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(fun_app$q, type, fun_app$q: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff('#skF_144', type, '#skF_144': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(comp_update$, type, comp_update$: ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(member$i, type, member$i: (A$ * A_set$) > $o).
% 33.85/15.04  tff(functor$e, type, functor$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(nTDom$c, type, nTDom$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$).
% 33.85/15.04  tff(oppositeCategory$, type, oppositeCategory$: A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$).
% 33.85/15.04  tff(catCod$e, type, catCod$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff('#skF_20', type, '#skF_20': (ZF_ZF_prod_bool_fun$ * ZF_ZF_prod_bool_fun$) > ZF_ZF_prod$).
% 33.85/15.04  tff(fun_app$z, type, fun_app$z: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$).
% 33.85/15.04  tff(nTCod_update$, type, nTCod_update$: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_12', type, '#skF_12': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_b_b_c_LSCategory_ext_Category_ext$ * A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ * A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(top$, type, top$: ZF_set$).
% 33.85/15.04  tff(catDom$f, type, catDom$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff('#skF_16', type, '#skF_16': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(mor$c, type, mor$c: Unit_unit_unit_Category_ext$ > Unit_set$).
% 33.85/15.04  tff('#skF_108', type, '#skF_108': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(category$b, type, category$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ > $o).
% 33.85/15.04  tff(member$b, type, member$b: (B_b_prod$ * B_b_prod_set$) > $o).
% 33.85/15.04  tff(fun_app$, type, fun_app$: (ZF_ZF_fun$ * ZF$) > ZF$).
% 33.85/15.04  tff(nTCod$c, type, nTCod$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_173', type, '#skF_173': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_66', type, '#skF_66': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(nTCompDefined$d, type, nTCompDefined$d: (A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ * A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(member$f, type, member$f: (A_ZF_fun$ * A_ZF_fun_set$) > $o).
% 33.85/15.04  tff(catCod$f, type, catCod$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(catDom$, type, catDom$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(idNatTrans$d, type, idNatTrans$d: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$).
% 33.85/15.04  tff('#skF_204', type, '#skF_204': (ZF_ZF_fun$ * ZF_ZF_fun$ * ZF$ * ZF$ * ZF$) > ZF$).
% 33.85/15.04  tff(nTDom$e, type, nTDom$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(uux$, type, uux$: A_b_b_c_LSCategory_ext_Category_ext$ > B_b_b_fun_fun$).
% 33.85/15.04  tff(functor_abbrev$, type, functor_abbrev$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$) > $o).
% 33.85/15.04  tff(idNatTrans$e, type, idNatTrans$e: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ > ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(inverse_rel$, type, inverse_rel$: (ZF_ZF_unit_Category_ext$ * ZF$) > ZF_bool_fun$).
% 33.85/15.04  tff('#skF_70', type, '#skF_70': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_28', type, '#skF_28': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A$).
% 33.85/15.04  tff(objIso$, type, objIso$: (ZF_ZF_unit_Category_ext$ * ZF$) > ZF_bool_fun$).
% 33.85/15.04  tff(hOMCollection$, type, hOMCollection$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$ * A$) > ZF_set$).
% 33.85/15.04  tff('#skF_89', type, '#skF_89': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff(category_axioms$, type, category_axioms$: A_b_b_c_LSCategory_ext_Category_ext$ > $o).
% 33.85/15.04  tff(nTCatDom$a, type, nTCatDom$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(constFunctor$a, type, constFunctor$a: (ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(homFtorMapContra$, type, homFtorMapContra$: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > A_ZF_fun$).
% 33.85/15.04  tff('#skF_71', type, '#skF_71': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(zFfunApp$, type, zFfunApp$: ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff('#skF_225', type, '#skF_225': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(restrict$f, type, restrict$f: (ZF_ZF_fun$ * ZF_set$) > ZF_ZF_fun$).
% 33.85/15.04  tff('#skF_29', type, '#skF_29': (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF$).
% 33.85/15.04  tff(equivalence_axioms$, type, equivalence_axioms$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(oppositeCategory$c, type, oppositeCategory$c: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(mapM$b, type, mapM$b: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(extensional$b, type, extensional$b: B_set$ > B_ZF_fun_set$).
% 33.85/15.04  tff('#skF_115', type, '#skF_115': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(id_update$, type, id_update$: ZF_ZF_fun_ZF_ZF_fun_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff('#skF_167', type, '#skF_167': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_148', type, '#skF_148': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_187', type, '#skF_187': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(pair$a, type, pair$a: (B$ * B$) > B_b_prod$).
% 33.85/15.04  tff('#skF_201', type, '#skF_201': (ZF$ * ZF_ZF_fun$ * ZF_ZF_fun$ * ZF$) > ZF$).
% 33.85/15.04  tff(mapM$, type, mapM$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B_ZF_fun$).
% 33.85/15.04  tff(mapO$e, type, mapO$e: (ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$ * ZF$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_156', type, '#skF_156': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff('#skF_120', type, '#skF_120': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(mapM$f, type, mapM$f: (A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$ * B$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_186', type, '#skF_186': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff('#skF_124', type, '#skF_124': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(functorComp$, type, functorComp$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_31', type, '#skF_31': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_171', type, '#skF_171': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(the$, type, the$: ZF_bool_fun$ > ZF$).
% 33.85/15.04  tff(restrict$, type, restrict$: (ZF_ZF_prod_ZF_fun$ * ZF_ZF_prod_set$ * ZF_ZF_prod$) > ZF$).
% 33.85/15.04  tff(uu$, type, uu$: B_set$ > B_bool_fun$).
% 33.85/15.04  tff(member$g, type, member$g: (A_b_fun$ * A_b_fun_set$) > $o).
% 33.85/15.04  tff('#skF_85', type, '#skF_85': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(mapM$d, type, mapM$d: (A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ * B$) > B$).
% 33.85/15.04  tff(category_ext$a, type, category_ext$a: (ZF_set$ * ZF_set$ * ZF_ZF_fun$ * ZF_ZF_fun$ * ZF_ZF_fun$ * ZF_ZF_ZF_fun_fun$ * Unit$) > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(collect$h, type, collect$h: A_b_fun_bool_fun$ > A_b_fun_set$).
% 33.85/15.04  tff(dom$, type, dom$: A_b_b_c_LSCategory_ext_Category_ext$ > B_a_fun$).
% 33.85/15.04  tff(comp$d, type, comp$d: ZF_ZF_fun$ > ZF_ZF_fun_ZF_ZF_fun_fun$).
% 33.85/15.04  tff('#skF_112', type, '#skF_112': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(homFtor$, type, homFtor$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(uuw$, type, uuw$: A_b_b_c_LSCategory_ext_Category_ext$ > B_b_prod_bool_fun$).
% 33.85/15.04  tff(natTransP$d, type, natTransP$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_13', type, '#skF_13': (B_bool_fun$ * B_bool_fun$) > B$).
% 33.85/15.04  tff('#skF_51', type, '#skF_51': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_145', type, '#skF_145': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(compDefined$a, type, compDefined$a: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > B_bool_fun$).
% 33.85/15.04  tff(catCod$c, type, catCod$c: ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(elem$, type, elem$: ZF$ > ZF_bool_fun$).
% 33.85/15.04  tff(nTCod_update$a, type, nTCod_update$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(category$, type, category$: A_b_b_c_LSCategory_ext_Category_ext$ > $o).
% 33.85/15.04  tff(fun_app$ab, type, fun_app$ab: (B_a_fun$ * B$) > A$).
% 33.85/15.04  tff('#skF_224', type, '#skF_224': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff(homFtorMap$, type, homFtorMap$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > B_ZF_fun$).
% 33.85/15.04  tff('#skF_135', type, '#skF_135': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(nTCod$e, type, nTCod$e: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_176', type, '#skF_176': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(makeCat$c, type, makeCat$c: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(cod_update$, type, cod_update$: ZF_ZF_fun_ZF_ZF_fun_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(functorExt$a, type, functorExt$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(uuh$, type, uuh$: B_b_prod_set$ > B_b_prod_bool_fun$).
% 33.85/15.04  tff('#skF_18', type, '#skF_18': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(inverse$, type, inverse$: ZF_ZF_unit_Category_ext$ > ZF_ZF_fun$).
% 33.85/15.04  tff(mapM$a, type, mapM$a: (ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ * ZF$) > Unit$).
% 33.85/15.04  tff(obj$a, type, obj$a: A_b_b_c_LSCategory_ext_Category_ext$ > A_set$).
% 33.85/15.04  tff('#skF_81', type, '#skF_81': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff(mapsTo$c, type, mapsTo$c: (Unit_unit_unit_Category_ext$ * Unit$ * Unit$ * Unit$) > $o).
% 33.85/15.04  tff('#skF_136', type, '#skF_136': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_39', type, '#skF_39': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(nTCatDom$c, type, nTCatDom$c: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff('#skF_25', type, '#skF_25': (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF$).
% 33.85/15.04  tff('#skF_151', type, '#skF_151': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_61', type, '#skF_61': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff(nTCod$d, type, nTCod$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$).
% 33.85/15.04  tff(nTCod$, type, nTCod$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$).
% 33.85/15.04  tff('#skF_208', type, '#skF_208': (ZF_set_ZF_set_fun$ * ZF_set_ZF_set_fun$ * ZF_ZF_unit_Category_ext$ * ZF_set$ * ZF_ZF_unit_Category_ext$) > ZF_set$).
% 33.85/15.04  tff(nTCatDom$f, type, nTCatDom$f: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(functor_comp_def$c, type, functor_comp_def$c: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff(extensional$a, type, extensional$a: A_set$ > A_ZF_fun_set$).
% 33.85/15.04  tff(nt_abbrev$a, type, nt_abbrev$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(mapM$e, type, mapM$e: (ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$ * ZF$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(member$l, type, member$l: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$) > $o).
% 33.85/15.04  tff('#skF_53', type, '#skF_53': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > B$).
% 33.85/15.04  tff(natTransP$b, type, natTransP$b: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_68', type, '#skF_68': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(mapM$c, type, mapM$c: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$ * ZF$) > B$).
% 33.85/15.04  tff(uua$, type, uua$: ZF_set$ > ZF_bool_fun$).
% 33.85/15.04  tff(nt_abbrev$c, type, nt_abbrev$c: (A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ * A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ * A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$) > $o).
% 33.85/15.04  tff('#skF_188', type, '#skF_188': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_141', type, '#skF_141': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(uug$, type, uug$: ZF_ZF_prod_set$ > ZF_ZF_prod_bool_fun$).
% 33.85/15.04  tff('#skF_104', type, '#skF_104': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff('#skF_138', type, '#skF_138': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(fun_app$ae, type, fun_app$ae: (B_set_b_set_fun$ * B_set$) > B_set$).
% 33.85/15.04  tff(natTransMap$c, type, natTransMap$c: (ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ * ZF$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(compDefined$c, type, compDefined$c: (Unit_unit_unit_Category_ext$ * Unit$ * Unit$) > $o).
% 33.85/15.04  tff('#skF_193', type, '#skF_193': (ZF_ZF_unit_Category_ext$ * ZF$ * ZF$) > ZF$).
% 33.85/15.04  tff(homFtorContra$, type, homFtorContra$: (A_b_b_c_LSCategory_ext_Category_ext$ * A$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_83', type, '#skF_83': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(uuy$, type, uuy$: ZF_ZF_unit_Category_ext$ > ZF_ZF_prod_bool_fun$).
% 33.85/15.04  tff(member$c, type, member$c: (ZF$ * ZF_set$) > $o).
% 33.85/15.04  tff(extCategory$a, type, extCategory$a: ZF_ZF_unit_Category_ext$ > $o).
% 33.85/15.04  tff(mor_update$, type, mor_update$: ZF_set_ZF_set_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(oppositeCategory$b, type, oppositeCategory$b: ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff(member$a, type, member$a: (ZF_ZF_prod$ * ZF_ZF_prod_set$) > $o).
% 33.85/15.04  tff('#skF_129', type, '#skF_129': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff(fun_app$c, type, fun_app$c: (B_b_prod_bool_fun$ * B_b_prod$) > $o).
% 33.85/15.04  tff('#skF_220', type, '#skF_220': (ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun$) > ZF_ZF_fun$).
% 33.85/15.04  tff(compDefined$, type, compDefined$: (ZF_ZF_unit_Category_ext$ * ZF$) > ZF_bool_fun$).
% 33.85/15.04  tff(extensional$d, type, extensional$d: ZF_ZF_prod_set$ > ZF_ZF_prod_ZF_fun_set$).
% 33.85/15.04  tff(uui$, type, uui$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(more$d, type, more$d: A_b_b_c_LSCategory_ext_Category_ext$ > B_c_LSCategory_ext$).
% 33.85/15.04  tff(identityFunctor$a, type, identityFunctor$a: ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(case_prod$a, type, case_prod$a: B_b_b_fun_fun$ > B_b_prod_b_fun$).
% 33.85/15.04  tff(nTCatCod$c, type, nTCatCod$c: ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff('#skF_125', type, '#skF_125': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(nTCod$b, type, nTCod$b: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(more_update$, type, more_update$: (Unit_unit_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(natTransExt$, type, natTransExt$: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff(collect$c, type, collect$c: ZF_bool_fun$ > ZF_set$).
% 33.85/15.04  tff(natTransP$, type, natTransP$: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_110', type, '#skF_110': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(natTrans$f, type, natTrans$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_118', type, '#skF_118': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff(fun_app$t, type, fun_app$t: (B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$ * B$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_103', type, '#skF_103': ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF$).
% 33.85/15.04  tff(nTCompDefined$a, type, nTCompDefined$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$).
% 33.85/15.04  tff(functor_ext$a, type, functor_ext$a: (A_b_b_c_LSCategory_ext_Category_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ * B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$ * Unit$) > A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(uuk$, type, uuk$: ZF_ZF_unit_Category_ext$ > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(more$c, type, more$c: A_b_b_c_LSCategory_ext_Category_ext$ > C$).
% 33.85/15.04  tff('#skF_24', type, '#skF_24': (ZF_bool_fun$ * ZF_bool_fun$) > ZF$).
% 33.85/15.04  tff('#skF_55', type, '#skF_55': A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(functorM$, type, functorM$: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(mapO$a, type, mapO$a: (A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$ * A$) > A$).
% 33.85/15.04  tff(idNatTrans$c, type, idNatTrans$c: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(preFunctor$a, type, preFunctor$a: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff('#skF_14', type, '#skF_14': (B_bool_fun$ * B_bool_fun$) > B$).
% 33.85/15.04  tff(constFunctor$, type, constFunctor$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff('#skF_58', type, '#skF_58': ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(functorM_axioms$, type, functorM_axioms$: ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(uuq$, type, uuq$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A$) > ZF_bool_fun$).
% 33.85/15.04  tff(mor_update$a, type, mor_update$a: B_set_b_set_fun$ > A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$).
% 33.85/15.04  tff(uum$, type, uum$: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > A_ZF_fun$).
% 33.85/15.04  tff('#skF_228', type, '#skF_228': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff(nTCompDefined$b, type, nTCompDefined$b: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ * ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(uun$, type, uun$: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff(nTCompDefined$, type, nTCompDefined$: (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(isZFfun$, type, isZFfun$: ZF_bool_fun$).
% 33.85/15.04  tff('#skF_17', type, '#skF_17': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_175', type, '#skF_175': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_62', type, '#skF_62': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff(catExp$a, type, catExp$a: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(mor$a, type, mor$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$).
% 33.85/15.04  tff('#skF_185', type, '#skF_185': ZF_ZF_unit_Category_ext$ > Unit$).
% 33.85/15.04  tff('#skF_98', type, '#skF_98': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff('#skF_37', type, '#skF_37': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_190', type, '#skF_190': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(uue$, type, uue$: A_ZF_fun_set$ > A_ZF_fun_bool_fun$).
% 33.85/15.04  tff(natTransComp$a, type, natTransComp$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_7', type, '#skF_7': (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(category$a, type, category$a: ZF_ZF_unit_Category_ext$ > $o).
% 33.85/15.04  tff('#skF_67', type, '#skF_67': ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff(natTransComp$, type, natTransComp$: (ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(unitFunctor$, type, unitFunctor$: ZF_ZF_unit_Category_ext$ > ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(isomorphism$a, type, isomorphism$a: ZF_ZF_unit_Category_ext$ > ZF_bool_fun$).
% 33.85/15.04  tff(fun_app$m, type, fun_app$m: (B_b_b_fun_fun$ * B$) > B_b_fun$).
% 33.85/15.04  tff(nTDom$b, type, nTDom$b: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(unity$, type, unity$: Unit$).
% 33.85/15.04  tff(cod$b, type, cod$b: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$).
% 33.85/15.04  tff(fun_app$l, type, fun_app$l: (B_b_fun$ * B$) > B$).
% 33.85/15.04  tff(more_update$a, type, more_update$a: Unit_unit_fun$ > ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$).
% 33.85/15.04  tff('#skF_114', type, '#skF_114': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > B$).
% 33.85/15.04  tff(functor$f, type, functor$f: A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(catDom_update$, type, catDom_update$: ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$).
% 33.85/15.04  tff(fun_app$x, type, fun_app$x: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff('#skF_43', type, '#skF_43': ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_132', type, '#skF_132': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(member$n, type, member$n: (B_b_prod_b_fun$ * B_b_prod_b_fun_set$) > $o).
% 33.85/15.04  tff(nTCatDom$d, type, nTCatDom$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff(image$, type, image$: (ZF_ZF_set_fun$ * ZF_set$) > ZF_set_set$).
% 33.85/15.04  tff(natTrans$, type, natTrans$: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$).
% 33.85/15.04  tff(nTCatCod$d, type, nTCatCod$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_b_b_c_LSCategory_ext_Category_ext$).
% 33.85/15.04  tff('#skF_219', type, '#skF_219': (ZF_ZF_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_fun_ZF_ZF_fun_fun$ * ZF_ZF_unit_Category_ext$) > ZF_ZF_fun$).
% 33.85/15.04  tff(natTransComp$d, type, natTransComp$d: (ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$ * ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$) > ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$).
% 33.85/15.04  tff(inverse$a, type, inverse$a: (A_b_b_c_LSCategory_ext_Category_ext$ * B$) > B$).
% 33.85/15.04  tff(oppositeCategory$a, type, oppositeCategory$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$ > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff(member$, type, member$: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$) > $o).
% 33.85/15.04  tff(catExp$c, type, catExp$c: (A_b_b_c_LSCategory_ext_Category_ext$ * ZF_ZF_unit_Category_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$).
% 33.85/15.04  tff('#skF_159', type, '#skF_159': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(nTCod$a, type, nTCod$a: ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ > ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$).
% 33.85/15.04  tff(compDefined$b, type, compDefined$b: (ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$) > $o).
% 33.85/15.04  tff(fun_app$a, type, fun_app$a: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$) > $o).
% 33.85/15.04  tff(functor$a, type, functor$a: ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ > $o).
% 33.85/15.04  tff(set$a, type, set$a: ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff(functor_abbrev$a, type, functor_abbrev$a: (ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$ * ZF_ZF_unit_Category_ext$ * Unit_unit_unit_Category_ext$) > $o).
% 33.85/15.04  tff(uud$, type, uud$: B_a_fun_set$ > B_a_fun_bool_fun$).
% 33.85/15.04  tff(fun_app$y, type, fun_app$y: (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$ * A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$) > A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$).
% 33.85/15.04  tff(functorM_axioms$a, type, functorM_axioms$a: A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$).
% 33.85/15.04  tff('#skF_63', type, '#skF_63': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$ > A$).
% 33.85/15.04  tff('#skF_169', type, '#skF_169': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff(natTrans$b, type, natTrans$b: ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$ > $o).
% 33.85/15.04  tff('#skF_213', type, '#skF_213': (ZF_ZF_ZF_fun_fun$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$ * ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$) > ZF_ZF_ZF_fun_fun$).
% 33.85/15.04  tff(more$e, type, more$e: ZF_ZF_unit_Category_ext$ > Unit$).
% 33.85/15.04  tff(explode$, type, explode$: ZF_ZF_set_fun$).
% 33.85/15.04  tff(mor$, type, mor$: A_b_b_c_LSCategory_ext_Category_ext$ > B_set$).
% 33.85/15.04  tff('#skF_168', type, '#skF_168': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_174', type, '#skF_174': ZF_ZF_unit_Category_ext$ > ZF$).
% 33.85/15.04  tff('#skF_210', type, '#skF_210': (ZF_ZF_unit_Category_ext$ * ZF_set_ZF_set_fun$ * ZF_set_ZF_set_fun$ * ZF_ZF_unit_Category_ext$ * ZF_set$) > ZF_set$).
% 33.85/15.04  tff(natTransMap$d, type, natTransMap$d: A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$ > A_b_fun$).
% 33.85/15.04  tff('#skF_9', type, '#skF_9': (ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$ * ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$ * ZF_ZF_unit_Category_ext$ * ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$) > ZF_ZF_unit_Category_ext$).
% 33.85/15.04  tff('#skF_122', type, '#skF_122': A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ > A$).
% 33.85/15.04  tff('#skF_134', type, '#skF_134': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  tff(the$a, type, the$a: B_bool_fun$ > B$).
% 33.85/15.04  tff(mapsTo$, type, mapsTo$: (A_b_b_c_LSCategory_ext_Category_ext$ * B$ * A$) > A_bool_fun$).
% 33.85/15.04  tff('#skF_211', type, '#skF_211': (A_b_b_c_LSCategory_ext_Category_ext$ * B_set_b_set_fun$ * B_set_b_set_fun$ * A_b_b_c_LSCategory_ext_Category_ext$ * B_set$) > B_set$).
% 33.85/15.04  tff('#skF_79', type, '#skF_79': ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$ > ZF$).
% 33.85/15.04  tff('#skF_117', type, '#skF_117': (A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$ * ZF$) > A$).
% 33.85/15.04  tff(restrict$b, type, restrict$b: (B_ZF_fun$ * B_set$) > B_ZF_fun$).
% 33.85/15.04  tff('#skF_165', type, '#skF_165': A_b_b_c_LSCategory_ext_Category_ext$ > A$).
% 33.85/15.04  tff('#skF_161', type, '#skF_161': A_b_b_c_LSCategory_ext_Category_ext$ > B$).
% 33.85/15.04  
% 33.85/15.05  tff(f_322, axiom, (![A__questionmark_v0:A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$]: (nTCatDom$(A__questionmark_v0) = nTCatDom$(makeNT$(A__questionmark_v0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom58)).
% 33.85/15.05  tff(f_200, axiom, (![A__questionmark_v0:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v1:B$]: (fun_app$t(yFtorNT$a(A__questionmark_v0), A__questionmark_v1) = makeNT$(yFtorNT$(A__questionmark_v0, A__questionmark_v1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom40)).
% 33.85/15.05  tff(f_194, axiom, (![A__questionmark_v0:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v1:B$]: (nTCatDom$(fun_app$t(yFtorNT$a(A__questionmark_v0), A__questionmark_v1)) = fun_app$s(oppositeCategory$, A__questionmark_v0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom38)).
% 33.85/15.05  tff(f_163, negated_conjecture, ~(nTCatDom$(yFtorNT$(c$, f$)) = catDom$(fun_app$r(nTCod$, yFtorNT$(c$, f$)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture27)).
% 33.85/15.05  tff(f_173, axiom, functor_abbrev$(fun_app$r(nTCod$, yFtorNT$(c$, f$)), fun_app$s(oppositeCategory$, c$), set$), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom32)).
% 33.85/15.05  tff(f_448, axiom, (![A__questionmark_v0:A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$, A__questionmark_v1:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v2:ZF_ZF_unit_Category_ext$]: (functor_abbrev$(A__questionmark_v0, A__questionmark_v1, A__questionmark_v2) <=> ((fun_app$a(functor$, A__questionmark_v0) & (catDom$(A__questionmark_v0) = A__questionmark_v1)) & (catCod$(A__questionmark_v0) = A__questionmark_v2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom75)).
% 33.85/15.05  tff(c_174, plain, (![A__questionmark_v0_133:A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$]: (nTCatDom$(makeNT$(A__questionmark_v0_133))=nTCatDom$(A__questionmark_v0_133))), inference(cnfTransformation, [status(thm)], [f_322])).
% 33.85/15.05  tff(c_126, plain, (![A__questionmark_v0_84:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v1_85:B$]: (fun_app$t(yFtorNT$a(A__questionmark_v0_84), A__questionmark_v1_85)=makeNT$(yFtorNT$(A__questionmark_v0_84, A__questionmark_v1_85)))), inference(cnfTransformation, [status(thm)], [f_200])).
% 33.85/15.05  tff(c_122, plain, (![A__questionmark_v0_80:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v1_81:B$]: (nTCatDom$(fun_app$t(yFtorNT$a(A__questionmark_v0_80), A__questionmark_v1_81))=fun_app$s(oppositeCategory$, A__questionmark_v0_80))), inference(cnfTransformation, [status(thm)], [f_194])).
% 33.85/15.05  tff(c_4440, plain, (![A__questionmark_v0_80:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v1_81:B$]: (nTCatDom$(yFtorNT$(A__questionmark_v0_80, A__questionmark_v1_81))=fun_app$s(oppositeCategory$, A__questionmark_v0_80))), inference(demodulation, [status(thm), theory('equality')], [c_174, c_126, c_122])).
% 33.85/15.05  tff(c_100, plain, (catDom$(fun_app$r(nTCod$, yFtorNT$(c$, f$)))!=nTCatDom$(yFtorNT$(c$, f$))), inference(cnfTransformation, [status(thm)], [f_163])).
% 33.85/15.05  tff(c_4445, plain, (catDom$(fun_app$r(nTCod$, yFtorNT$(c$, f$)))!=fun_app$s(oppositeCategory$, c$)), inference(demodulation, [status(thm), theory('equality')], [c_4440, c_100])).
% 33.85/15.05  tff(c_110, plain, (functor_abbrev$(fun_app$r(nTCod$, yFtorNT$(c$, f$)), fun_app$s(oppositeCategory$, c$), set$)), inference(cnfTransformation, [status(thm)], [f_173])).
% 33.85/15.05  tff(c_240, plain, (![A__questionmark_v0_172:A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$, A__questionmark_v1_173:A_b_b_c_LSCategory_ext_Category_ext$, A__questionmark_v2_174:ZF_ZF_unit_Category_ext$]: (catDom$(A__questionmark_v0_172)=A__questionmark_v1_173 | ~functor_abbrev$(A__questionmark_v0_172, A__questionmark_v1_173, A__questionmark_v2_174))), inference(cnfTransformation, [status(thm)], [f_448])).
% 33.85/15.05  tff(c_8173, plain, (catDom$(fun_app$r(nTCod$, yFtorNT$(c$, f$)))=fun_app$s(oppositeCategory$, c$)), inference(resolution, [status(thm)], [c_110, c_240])).
% 33.85/15.05  tff(c_8180, plain, $false, inference(negUnitSimplification, [status(thm)], [c_4445, c_8173])).
% 33.85/15.05  % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------