gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

serre.lisp #100

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFUN FIBRATION-DTAU-D ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC CAT::UTOTAL :TRGT CAT::UTOTAL :DEGR -1 :INTR ; (CAT::FIBRATION-DTAU-D-INTR CAT::FIBRATION) :STRT :GNRT ; :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN LEFT-SERRE-EFHM ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (CAT::BUILD-HMEQ :LRDCT ; (CAT::TRIVIAL-RDCT ; (CAT::FIBRATION-TOTAL CAT::FIBRATION)) ; :RRDCT (CAT::BROWN-REDUCTION CAT::FIBRATION))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).

; in: DEFUN FIBRATION-TOTAL-EFHM ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (CAT::CMPS (CAT::LEFT-SERRE-EFHM CAT::FIBRATION) ; (CAT::RIGHT-SERRE-EFHM CAT::FIBRATION))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).

; in: DEFMETHOD SEARCH-EFHM (T (EQL (QUOTE FIBRATION-TOTAL))) ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (CAT::FIBRATION-TOTAL-EFHM (SECOND (CAT::ORGN CAT::SMST)))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).