--#include "MBSet.alfa" --#include "NitP.alfa" package Algebraic1Par where Sig :: Type = data nil | nonrec (a::Set) (fi::a -> Sig) | par (fi'::Sig) | rec (fi'::Sig) open NitP use Nit open NitP1 use Sigma1 F (fi::Sig)(X::Set) :: Nit one = case fi of { (nil) -> \(p::Set) -> Unit; (nonrec A f) -> Sigma1 A (\(a::A) -> F (f a) X); (par fi') -> \(p::Set) -> And p (F fi' X p); (rec fi') -> \(p::Set) -> And X (F fi' X p);} F1 (fi::Sig)(X::Set)(Y::Set)(f::X -> Y)(p::Set)(x::F fi X p) :: F fi Y p = case fi of { (nil) -> tt@_; (nonrec A f') -> case x of { (si a b) -> si@_ a (F1 (f' a) X Y f p b);}; (par fi') -> case x of { (Pair a b) -> Pair@_ a (F1 fi' X Y f p b);}; (rec fi') -> case x of { (Pair a b) -> Pair@_ (f a) (F1 fi' X Y f p b);};} T (fi::Sig)(p::Set) :: Set = data Intro (im::F fi (T fi p) p) out (fi::Sig)(p::Set)(x::T fi p) :: F fi (T fi p) p = case x of { (Intro im) -> im;} It (fi::Sig)(p::Set)(C::Set)(d::F fi C p -> C) :: T fi p -> C = \(x::T fi p) -> case x of { (Intro im) -> d (F1 fi (T fi p) C (It fi p C d) p im);} F2 (P1::Set) (P2::Set) (R1::Set) (R2::Set) (fi::Sig) (pa::P1 -> P2) (re::R1 -> R2) (xs::F fi R1 P1) :: F fi R2 P2 = case fi of { (nil) -> case xs of { (tt) -> tt@_;}; (nonrec a' f') -> case xs of { (si a b) -> si@_ a (F2 P1 P2 R1 R2 (f' a) pa re b);}; (par fi') -> case xs of { (Pair a b) -> Pair@_ (pa a) (F2 P1 P2 R1 R2 fi' pa re b);}; (rec fi') -> case xs of { (Pair a b) -> Pair@_ (re a) (F2 P1 P2 R1 R2 fi' pa re b);};} d_map1 (X::Set)(a::Set)(b::Set)(f::a -> b)(fi::Sig)(xs::F fi X a) :: F fi X b = case fi of { (nil) -> case xs of { (tt) -> tt@_;}; (nonrec a' fi') -> case xs of { (si a0 b') -> si@_ a0 (d_map1 X a b f (fi' a0) b');}; (par fi') -> case xs of { (Pair a' b') -> Pair@_ (f a') (d_map1 X a b f fi' b');}; (rec fi') -> case xs of { (Pair a' b') -> Pair@_ a' (d_map1 X a b f fi' b');};} d_map2 (a::Set)(b::Set)(f::a -> b)(fi::Sig)(xs::F fi (T fi b) a) :: T fi b = Intro@_ (d_map1 (T fi b) a b f fi xs) map (a::Set)(b::Set)(f::a -> b)(fi::Sig)(xs::T fi a) :: T fi b = It fi a (T fi b) (d_map2 a b f fi) xs open Algebraic1Par use Sig, T Lcons :: Set = data Nil | Cons sigmaL (c::Lcons) :: Sig = case c of { (Nil) -> nil@_; (Cons) -> par@_ (rec@_ nil@_);} spL :: Sig = nonrec@_ Lcons sigmaL IL (a::Set) :: Set = T spL a {-# Alfa unfoldgoals off brief on hidetypeannots off wide typesignatures nd hiding on var "Unit" as "()" con "tt" as "*" var "Sigma" quantifier domain on as "S" with symbolfont var "fi" as "F" with symbolfont var "fi'" as "F1" with symbolfont var "And" infix rightassoc as "´" with symbolfont con "AndI" tuple con "Pair" tuple con "Zero" as "0" var "nitLiftSigma" as "S#" with symbolfont var "one" as "1" con "si" tuple var "out" hide 2 var "d_map1" hide 3 var "Sigma1" as "S1" with symbolfont var "F2" hide 4 #-}