slowness issue for https://github.com/Gabriel439/Haskell-Morte-Library

AND

-- #AND: #Prop -> #Prop -> #Prop
\(A: #Prop )-> \(B: #Prop )-> 
\/(AND: #Prop )->
\/(Intro: A -> B -> AND)->
AND

AND-Intro

-- #AND-Intro: \/(A B: #Prop )-> A -> B -> #AND A B

-- arguments
\(A: #Prop )->
\(B: #Prop )->
\(a: A)->
\(b: B)->

-- encoding
\(AND: #Prop )->
\(Intro: A -> B -> AND)->
Intro a b

IsoAAOk

-- #IsoAAOk: \/(A B: #Setoid)-> \/(fab: IsoAB A B)-> \/(fba: IsoBA A B)-> #Prop

-- A, B: #Setoid
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
\(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
\(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
\(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->

\/(a: A)-> \/(aok: AOk a)-> AEqu a (isoBA (isoAB a))

IsoAB

-- #IsoAB: #Setoid -> #Setoid -> #Setoid
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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)->
#SetoidHom A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym

IsoABOk

-- #IsoABOk: \/(A B: #Setoid)-> \/(fab: #IsoAB A B)-> #Prop
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
#SetoidHomOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB

IsoBA

-- #IsoBA: #Setoid -> #Setoid -> #Setoid
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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)->
#SetoidHom B BOk BEqu BRefl BTrans BSym A AOk AEqu ARefl ATrans ASym 

IsoBAOk

-- #IsoBAOk: \/(A B: #Setoid)-> \/(fba: #IsoBA A B)-> #Prop
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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)->
\(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
#SetoidHomOk B BOk BEqu BRefl BTrans BSym A AOk AEqu ARefl ATrans ASym isoBA

IsoBBOk

-- #IsoBBOk: \/(A B: #Setoid)-> \/(fab: IsoAB A B)-> \/(fba: IsoBA A B)-> #Prop

-- A, B: #Setoid
\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
\(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
\(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
\(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->

\/(b: B)-> \/(bok: BOk b)-> BEqu b (isoAB (isoBA b))

Prop

-- #Prop: BOX
*

SetoidHom

-- #SetoidHom: 
-- \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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)->
-- #Star

\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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)->
A -> B

SetoidHomOk

-- #SetoidHomOk: 
-- \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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)->
-- \/(f: #SetoidHom A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
-- #Prop

\(A: #Star )-> \(AOk: A -> #Prop ) -> \(AEqu: A -> A -> #Prop )-> \(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: #Star )-> \(BOk: B -> #Prop ) -> \(BEqu: B -> B -> #Prop )-> \(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)->

\(f: #SetoidHom A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->

#AND
(\/(a: A)-> \/(aok: AOk a)-> BOk (f a))
(\/(a1: A)-> \/(a1ok: AOk a1)-> \/(a2: A)-> \/(a2ok: AOk a2)-> AEqu a1 a2 -> BEqu (f a1) (f a2))

Shadow

-- #Shadow: #Star

-- Shadow: #Setoid
\/(Shadow: #Star )->
\/(ShadowOk: Shadow -> #Prop )->
\/(ShadowEqu: Shadow -> Shadow -> #Prop )->
\/(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\/(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- Lim in #Setoid by Shadow
Shadow

Shadow-Mk

-- #Shadow-Mk: #Setoid -> #Shadow

-- Arg: #Setoid
\(Arg: #Star )->
\(ArgOk: Arg -> #Prop )->
\(ArgEqu: Arg -> Arg -> #Prop )->
\(ArgRefl: \/(s: Arg)-> ArgEqu s s )->
\(ArgTrans: \/(s1: Arg)-> \/(s2: Arg)-> \/(s3: Arg)-> ArgEqu s1 s2 -> ArgEqu s2 s3 -> ArgEqu s1 s3)->
\(ArgSym: \/(s1: Arg)-> \/(s2: Arg)-> ArgEqu s1 s2 -> ArgEqu s2 s1)->

-- Shadow: #Setoid
\(Shadow: #Star )->
\(ShadowOk: Shadow -> #Prop )->
\(ShadowEqu: Shadow -> Shadow -> #Prop )->
\(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result
Mk Arg ArgOk ArgEqu ArgRefl ArgTrans ArgSym

Shadow-MkOk

-- #Shadow-MkOk: (Arg: #Setoid) -> #ShadowOk (#Shadow-Mk Arg)

-- Arg: #Setoid
\(Arg: #Star )->
\(ArgOk: Arg -> #Prop )->
\(ArgEqu: Arg -> Arg -> #Prop )->
\(ArgRefl: \/(s: Arg)-> ArgEqu s s )->
\(ArgTrans: \/(s1: Arg)-> \/(s2: Arg)-> \/(s3: Arg)-> ArgEqu s1 s2 -> ArgEqu s2 s3 -> ArgEqu s1 s3)->
\(ArgSym: \/(s1: Arg)-> \/(s2: Arg)-> ArgEqu s1 s2 -> ArgEqu s2 s1)->

-- #ShadowOk (shadow Arg)
#AND-Intro
(#ShadowOkOk (#Shadow-Mk Arg ArgOk ArgEqu ArgRefl ArgTrans ArgSym)) 
(#ShadowOkLim (#Shadow-Mk Arg ArgOk ArgEqu ArgRefl ArgTrans ArgSym))

-- #ShadowOkOk (shadow Arg)
(
-- Shadow: #Setoid
\(Shadow: #Star )->
\(ShadowOk: Shadow -> #Prop )->
\(ShadowEqu: Shadow -> Shadow -> #Prop )->
\(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result1
    MkOk Arg ArgOk ArgEqu ArgRefl ArgTrans ArgSym
)

-- OkLim
(
-- XShadow: #Setoid
\(XShadow: #Star )->
\(XShadowOk: XShadow -> #Prop )->
\(XShadowEqu: XShadow -> XShadow -> #Prop )->
\(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)->

-- constructor XMk: #GroupoidToSetoidMapping #Setoid XShadow
\(XMk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    XShadowEqu (XMk A AOk AEqu ARefl ATrans ASym) (XMk B BOk BEqu BRefl BTrans BSym)
)->

-- YShadow: #Setoid
\(YShadow: #Star )->
\(YShadowOk: YShadow -> #Prop )->
\(YShadowEqu: YShadow -> YShadow -> #Prop )->
\(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)->

-- constructor XMk: #GroupoidToSetoidMapping #Setoid YShadow
\(YMk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    YShadowEqu (YMk A AOk AEqu ARefl ATrans ASym) (YMk B BOk BEqu BRefl BTrans BSym)
)->

-- mor: #Mor (X,XMk) (Y,YMk) -- morphism
\(mor: #SetoidHom XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym)->
\(morOk: #SetoidHomOk XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym mor)->
\(morLim: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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)
)->

-- result2
    morLim Arg ArgOk ArgEqu ArgRefl ArgTrans ArgSym
)

ShadowEqu

-- #ShadowEqu: #Shadow -> #Shadow -> #Prop

\(shA: #Shadow )->
\(shB: #Shadow )->

-- Shadow: #Setoid
\/(Shadow: #Star )->
\/(ShadowOk: Shadow -> #Prop )->
\/(ShadowEqu: Shadow -> Shadow -> #Prop )->
\/(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\/(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result
ShadowEqu (shA Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (shB Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu)

ShadowOk

-- #ShadowOk: #Shadow -> #Prop

\(sh: #Shadow )->
#AND 
(#ShadowOkOk sh) 
(#ShadowOkLim sh)

ShadowOkLim

-- #ShadowOkLim: \/(sh: #Shadow )-> \/(shOk: #ShadowOkOk sh)-> #Prop

\(sh: #Shadow )->

-- XShadow: #Setoid
\/(XShadow: #Star )->
\/(XShadowOk: XShadow -> #Prop )->
\/(XShadowEqu: XShadow -> XShadow -> #Prop )->
\/(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)->

-- constructor XMk: #GroupoidToSetoidMapping #Setoid XShadow
\/(XMk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    XShadowEqu (XMk A AOk AEqu ARefl ATrans ASym) (XMk B BOk BEqu BRefl BTrans BSym)
)->

-- YShadow: #Setoid
\/(YShadow: #Star )->
\/(YShadowOk: YShadow -> #Prop )->
\/(YShadowEqu: YShadow -> YShadow -> #Prop )->
\/(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)->

-- constructor XMk: #GroupoidToSetoidMapping #Setoid YShadow
\/(YMk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    YShadowEqu (YMk A AOk AEqu ARefl ATrans ASym) (YMk B BOk BEqu BRefl BTrans BSym)
)->

-- mor: #Mor (X,XMk) (Y,YMk) -- morphism
\/(mor: #SetoidHom XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym)->
\/(morOk: #SetoidHomOk XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym mor)->
\/(morLim: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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)
)->

-- Lim property on cone
YShadowEqu
    (mor 
    (sh XShadow XShadowOk XShadowEqu XShadowRefl XShadowTrans XShadowSym XMk XMkOk XMkIsoEqu))
    (sh YShadow YShadowOk YShadowEqu YShadowRefl YShadowTrans YShadowSym YMk YMkOk YMkIsoEqu)
    

ShadowOkOk

-- #ShadowOkOk: #Shadow -> #Prop
\(sh: #Shadow ) ->

-- Shadow: #Setoid
\/(Shadow: #Star )->
\/(ShadowOk: Shadow -> #Prop )->
\/(ShadowEqu: Shadow -> Shadow -> #Prop )->
\/(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\/(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- Lim at #Prop level
ShadowOk (
    sh Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu
)

ShadowRefl

-- #ShadowRefl: \/(s: #Shadow)-> #ShadowEqu s s 

\(sh: #Shadow )->

-- Shadow: #Setoid
\(Shadow: #Star )->
\(ShadowOk: Shadow -> #Prop )->
\(ShadowEqu: Shadow -> Shadow -> #Prop )->
\(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result
ShadowRefl (sh Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu)

ShadowSym

-- #ShadowSym: \/(s1: #Shadow)-> \/(s2: #Shadow)-> #ShadowEqu s1 s2 -> #ShadowEqu s2 s1

\(sh1: #Shadow )->
\(sh2: #Shadow )->
\(shequ12: #ShadowEqu sh1 sh2)->

-- Shadow: #Setoid
\(Shadow: #Star )->
\(ShadowOk: Shadow -> #Prop )->
\(ShadowEqu: Shadow -> Shadow -> #Prop )->
\(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result
ShadowSym (sh1 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (sh2 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (shequ12 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) 

ShadowTrans

-- #ShadowTrans: \/(s1: #Shadow)-> \/(s2: #Shadow)-> \/(s3: #Shadow)-> #ShadowEqu s1 s2 -> #ShadowEqu s2 s3 -> #ShadowEqu s1 s3

\(sh1: #Shadow )->
\(sh2: #Shadow )->
\(sh3: #Shadow )->
\(shequ12: #ShadowEqu sh1 sh2)->
\(shequ23: #ShadowEqu sh2 sh3)->

-- Shadow: #Setoid
\(Shadow: #Star )->
\(ShadowOk: Shadow -> #Prop )->
\(ShadowEqu: Shadow -> Shadow -> #Prop )->
\(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)->

-- constructor Mk: #GroupoidToSetoidMapping #Setoid Shadow
\(Mk: 
    \/(A: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(AOk: A -> #Prop ) -> \/(AEqu: A -> A -> #Prop )-> \/(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: #Star )-> \/(BOk: B -> #Prop ) -> \/(BEqu: B -> B -> #Prop )-> \/(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: #IsoAB A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoABOk: #IsoABOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB)->
    \/(isoBA: #IsoBA A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym)->
    \/(isoBAOk: #IsoBAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoBA)->
    \/(isoAAOk: #IsoAAOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    \/(isoBBOk: #IsoBBOk A AOk AEqu ARefl ATrans ASym B BOk BEqu BRefl BTrans BSym isoAB isoABOk isoBA isoBAOk)->
    ShadowEqu (Mk A AOk AEqu ARefl ATrans ASym) (Mk B BOk BEqu BRefl BTrans BSym)
)->

-- result
ShadowTrans (sh1 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (sh2 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (sh3 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (shequ12 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu) (shequ23 Shadow ShadowOk ShadowEqu ShadowRefl ShadowTrans ShadowSym Mk MkOk MkIsoEqu)

Star

-- #Star: BOX
*