Skip to content

Instantly share code, notes, and snippets.

@zraffer

zraffer/AND

Created February 23, 2016 17:36
Show Gist options
  • Save zraffer/dc90b5d076eda6156277 to your computer and use it in GitHub Desktop.
Save zraffer/dc90b5d076eda6156277 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
AND
-- #AND: #Prop -> #Prop -> #Prop
\(A: #Prop )-> \(B: #Prop )->
\/(AND: #Prop )->
\/(Intro: A -> B -> AND)->
AND
Raw
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
Raw
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))
Raw
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
Raw
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
Raw
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
Raw
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
Raw
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))
Raw
Prop
-- #Prop: BOX
*
Raw
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
Raw
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))
Raw
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
Raw
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
Raw
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
)
Raw
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)
Raw
ShadowOk
-- #ShadowOk: #Shadow -> #Prop
\(sh: #Shadow )->
#AND
(#ShadowOkOk sh)
(#ShadowOkLim sh)
Raw
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)
Raw
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
)
Raw
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)
Raw
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)
Raw
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)
Raw
Star
-- #Star: BOX
*
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment