fast term

gistfile1.txt

λ(sh : ∀(Shadow : *) → ∀(ShadowOk : Shadow → *) → ∀(ShadowEqu : Shadow → Shadow → *) → ∀(ShadowRefl : ∀(s : Shadow) → ShadowEqu s s) → ∀(ShadowTrans : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ∀(s3 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s3 → ShadowEqu s1 s3) → ∀(ShadowSym : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s1) → ∀(Mk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → Shadow) → ∀(MkOk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ShadowOk (Mk A AOk AEqu ARefl ATrans ASym)) → ∀(MkIsoEqu : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ∀(B : *) → ∀(BOk : B → *) → ∀(BEqu : B → B → *) → ∀(BRefl : ∀(b : B) → BEqu b b) → ∀(BTrans : ∀(b1 : B) → ∀(b2 : B) → ∀(b3 : B) → BEqu b1 b2 → BEqu b2 b3 → BEqu b1 b3) → ∀(BSym : ∀(b1 : B) → ∀(b2 : B) → BEqu b1 b2 → BEqu b2 b1) → ∀(isoAB : A → B) → ∀(isoABOk : ∀(AND : *) → ∀(Intro : (∀(a : A) → ∀(aok : AOk a) → BOk (isoAB a)) → (∀(a1 : A) → ∀(a1ok : AOk a1) → ∀(a2 : A) → ∀(a2ok : AOk a2) → AEqu a1 a2 → BEqu (isoAB a1) (isoAB a2)) → AND) → AND) → ∀(isoBA : B → A) → ∀(isoBAOk : ∀(AND : *) → ∀(Intro : (∀(a : B) → ∀(aok : BOk a) → AOk (isoBA a)) → (∀(a1 : B) → ∀(a1ok : BOk a1) → ∀(a2 : B) → ∀(a2ok : BOk a2) → BEqu a1 a2 → AEqu (isoBA a1) (isoBA a2)) → AND) → AND) → ∀(isoAAOk : ∀(a : A) → ∀(aok : AOk a) → AEqu a (isoBA (isoAB a))) → ∀(isoBBOk : ∀(b : B) → ∀(bok : BOk b) → BEqu b (isoAB (isoBA b))) → ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)) → Shadow) → ∀(AND : *) → ∀(intro : ∀(a : ∀(Shadow : *) → ∀(ShadowOk : Shadow → *) → ∀(ShadowEqu : Shadow → Shadow → *) → ∀(ShadowRefl : ∀(s : Shadow) → ShadowEqu s s) → ∀(ShadowTrans : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ∀(s3 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s3 → ShadowEqu s1 s3) → ∀(ShadowSym : ∀(s1 : Shadow) → ∀(s2 : Shadow) → ShadowEqu s1 s2 → ShadowEqu s2 s1) → ∀(Mk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → Shadow) → ∀(MkOk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ShadowOk (Mk A AOk AEqu ARefl ATrans ASym)) → ∀(MkIsoEqu : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ∀(B : *) → ∀(BOk : B → *) → ∀(BEqu : B → B → *) → ∀(BRefl : ∀(b : B) → BEqu b b) → ∀(BTrans : ∀(b1 : B) → ∀(b2 : B) → ∀(b3 : B) → BEqu b1 b2 → BEqu b2 b3 → BEqu b1 b3) → ∀(BSym : ∀(b1 : B) → ∀(b2 : B) → BEqu b1 b2 → BEqu b2 b1) → ∀(isoAB : A → B) → ∀(isoABOk : ∀(AND : *) → ∀(Intro : (∀(a : A) → ∀(aok : AOk a) → BOk (isoAB a)) → (∀(a1 : A) → ∀(a1ok : AOk a1) → ∀(a2 : A) → ∀(a2ok : AOk a2) → AEqu a1 a2 → BEqu (isoAB a1) (isoAB a2)) → AND) → AND) → ∀(isoBA : B → A) → ∀(isoBAOk : ∀(AND : *) → ∀(Intro : (∀(a : B) → ∀(aok : BOk a) → AOk (isoBA a)) → (∀(a1 : B) → ∀(a1ok : BOk a1) → ∀(a2 : B) → ∀(a2ok : BOk a2) → BEqu a1 a2 → AEqu (isoBA a1) (isoBA a2)) → AND) → AND) → ∀(isoAAOk : ∀(a : A) → ∀(aok : AOk a) → AEqu a (isoBA (isoAB a))) → ∀(isoBBOk : ∀(b : B) → ∀(bok : BOk b) → BEqu b (isoAB (isoBA b))) → ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)) → ShadowOk (sh Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu)) → ∀(b : ∀(XShadow : *) → ∀(XShadowOk : XShadow → *) → ∀(XShadowEqu : XShadow → XShadow → *) → ∀(XShadowRefl : ∀(s : XShadow) → XShadowEqu s s) → ∀(XShadowTrans : ∀(s1 : XShadow) → ∀(s2 : XShadow) → ∀(s3 : XShadow) → XShadowEqu s1 s2 → XShadowEqu s2 s3 → XShadowEqu s1 s3) → ∀(XShadowSym : ∀(s1 : XShadow) → ∀(s2 : XShadow) → XShadowEqu s1 s2 → XShadowEqu s2 s1) → ∀(XMk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → XShadow) → ∀(XMkOk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → XShadowOk (XMk A AOk AEqu ARefl ATrans ASym)) → ∀(XMkIsoEqu : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ∀(B : *) → ∀(BOk : B → *) → ∀(BEqu : B → B → *) → ∀(BRefl : ∀(b : B) → BEqu b b) → ∀(BTrans : ∀(b1 : B) → ∀(b2 : B) → ∀(b3 : B) → BEqu b1 b2 → BEqu b2 b3 → BEqu b1 b3) → ∀(BSym : ∀(b1 : B) → ∀(b2 : B) → BEqu b1 b2 → BEqu b2 b1) → ∀(isoAB : A → B) → ∀(isoABOk : ∀(AND : *) → ∀(Intro : (∀(a : A) → ∀(aok : AOk a) → BOk (isoAB a)) → (∀(a1 : A) → ∀(a1ok : AOk a1) → ∀(a2 : A) → ∀(a2ok : AOk a2) → AEqu a1 a2 → BEqu (isoAB a1) (isoAB a2)) → AND) → AND) → ∀(isoBA : B → A) → ∀(isoBAOk : ∀(AND : *) → ∀(Intro : (∀(a : B) → ∀(aok : BOk a) → AOk (isoBA a)) → (∀(a1 : B) → ∀(a1ok : BOk a1) → ∀(a2 : B) → ∀(a2ok : BOk a2) → BEqu a1 a2 → AEqu (isoBA a1) (isoBA a2)) → AND) → AND) → ∀(isoAAOk : ∀(a : A) → ∀(aok : AOk a) → AEqu a (isoBA (isoAB a))) → ∀(isoBBOk : ∀(b : B) → ∀(bok : BOk b) → BEqu b (isoAB (isoBA b))) → XShadowEqu (XMk A AOk AEqu ARefl ATrans ASym) (XMk B BOk BEqu BRefl BTrans BSym)) → ∀(YShadow : *) → ∀(YShadowOk : YShadow → *) → ∀(YShadowEqu : YShadow → YShadow → *) → ∀(YShadowRefl : ∀(s : YShadow) → YShadowEqu s s) → ∀(YShadowTrans : ∀(s1 : YShadow) → ∀(s2 : YShadow) → ∀(s3 : YShadow) → YShadowEqu s1 s2 → YShadowEqu s2 s3 → YShadowEqu s1 s3) → ∀(YShadowSym : ∀(s1 : YShadow) → ∀(s2 : YShadow) → YShadowEqu s1 s2 → YShadowEqu s2 s1) → ∀(YMk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → YShadow) → ∀(YMkOk : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → YShadowOk (YMk A AOk AEqu ARefl ATrans ASym)) → ∀(YMkIsoEqu : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → ∀(B : *) → ∀(BOk : B → *) → ∀(BEqu : B → B → *) → ∀(BRefl : ∀(b : B) → BEqu b b) → ∀(BTrans : ∀(b1 : B) → ∀(b2 : B) → ∀(b3 : B) → BEqu b1 b2 → BEqu b2 b3 → BEqu b1 b3) → ∀(BSym : ∀(b1 : B) → ∀(b2 : B) → BEqu b1 b2 → BEqu b2 b1) → ∀(isoAB : A → B) → ∀(isoABOk : ∀(AND : *) → ∀(Intro : (∀(a : A) → ∀(aok : AOk a) → BOk (isoAB a)) → (∀(a1 : A) → ∀(a1ok : AOk a1) → ∀(a2 : A) → ∀(a2ok : AOk a2) → AEqu a1 a2 → BEqu (isoAB a1) (isoAB a2)) → AND) → AND) → ∀(isoBA : B → A) → ∀(isoBAOk : ∀(AND : *) → ∀(Intro : (∀(a : B) → ∀(aok : BOk a) → AOk (isoBA a)) → (∀(a1 : B) → ∀(a1ok : BOk a1) → ∀(a2 : B) → ∀(a2ok : BOk a2) → BEqu a1 a2 → AEqu (isoBA a1) (isoBA a2)) → AND) → AND) → ∀(isoAAOk : ∀(a : A) → ∀(aok : AOk a) → AEqu a (isoBA (isoAB a))) → ∀(isoBBOk : ∀(b : B) → ∀(bok : BOk b) → BEqu b (isoAB (isoBA b))) → YShadowEqu (YMk A AOk AEqu ARefl ATrans ASym) (YMk B BOk BEqu BRefl BTrans BSym)) → ∀(mor : XShadow → YShadow) → ∀(morOk : ∀(AND : *) → ∀(Intro : (∀(a : XShadow) → ∀(aok : XShadowOk a) → YShadowOk (mor a)) → (∀(a1 : XShadow) → ∀(a1ok : XShadowOk a1) → ∀(a2 : XShadow) → ∀(a2ok : XShadowOk a2) → XShadowEqu a1 a2 → YShadowEqu (mor a1) (mor a2)) → AND) → AND) → ∀(morLim : ∀(A : *) → ∀(AOk : A → *) → ∀(AEqu : A → A → *) → ∀(ARefl : ∀(a : A) → AEqu a a) → ∀(ATrans : ∀(a1 : A) → ∀(a2 : A) → ∀(a3 : A) → AEqu a1 a2 → AEqu a2 a3 → AEqu a1 a3) → ∀(ASym : ∀(a1 : A) → ∀(a2 : A) → AEqu a1 a2 → AEqu a2 a1) → YShadowEqu (mor (XMk A AOk AEqu ARefl ATrans ASym)) (YMk A AOk AEqu ARefl ATrans ASym)) → YShadowEqu (mor (sh XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym XMk XMkOk XMkIsoEqu)) (sh YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym YMk YMkOk YMkIsoEqu)) → AND) → AND