--#include "../Prelude.alfa" Sig :: Type = data nil | nonrec (D::Datoid) (g::D.Elem -> Sig) | rec (fi'::Sig) F (fi::Sig)(X::Set) :: Set = case fi of { (nil) -> Unit; (nonrec D g) -> Sum D.Elem (\(d::D.Elem) -> F (g d) X); (rec fi') -> Times X (F fi' X);} F1 (fi::Sig)(a::Set)(b::Set)(f::a -> b) :: F fi a -> F fi b = case fi of { (nil) -> id Unit; (nonrec D fi') -> mapSum D.Elem (\(d::D.Elem) -> F (fi' d) a) (\(d::D.Elem) -> F (fi' d) b) (\(d::D.Elem) -> F1 (fi' d) a b f); (rec fi') -> mapTimes a b (F fi' a) (F fi' b) f (F1 fi' a b f);} T (fi::Sig) :: Set = data Intro (im::F fi (T fi)) out (fi::Sig)(i::T fi) :: F fi (T fi) = case i of { (Intro im) -> im;} It (fi::Sig)(C::Set)(d::F fi C -> C) :: T fi -> C = \(h::T fi) -> d (F1 fi (T fi) C (It fi C d) (out fi h)) FIH (fi::Sig)(Y::Set)(C::Y -> Set) :: F fi Y -> Set = case fi of { (nil) -> \(u::Unit) -> Unit; (nonrec D fi') -> \(yz::Sum D.Elem (\(d::D.Elem) -> F (fi' d) Y)) -> FIH (fi' yz.fst) Y C yz.snd; (rec fi') -> \(yz::Times Y (F fi' Y)) -> Times (C yz.fst) (FIH fi' Y C yz.snd);} FIH1 (fi::Sig)(Y::Set)(C::Y -> Set)(r::(y::Y) -> C y) :: (x::F fi Y) -> FIH fi Y C x = case fi of { (nil) -> id Unit; (nonrec D g) -> \(yz::Sum D.Elem (\(d::D.Elem) -> F (g d) Y)) -> FIH1 (g yz.fst) Y C r yz.snd; (rec fi') -> \(yz::F (rec@_ fi') Y) -> pair (C yz.fst) (FIH fi' Y C yz.snd) (r yz.fst) (FIH1 fi' Y C r yz.snd);} R (fi::Sig) (C::T fi -> Set) (d::(y::F fi (T fi)) -> FIH fi (T fi) C y -> C (Intro@_ y)) (x::T fi) :: C x = case x of { (Intro im) -> d im (FIH1 fi (T fi) C (R fi C d) im);} R' (fi::Sig) (C::T fi -> Set) (d::F fi (Sum (T fi) C) -> Sum (T fi) C) (x::T fi) :: Sum (T fi) C = It fi (Sum (T fi) C) d x MIt (fi::Sig)(G::Set)(s::(X::Set) -> (X -> G) -> F fi X -> G)(x::T fi) :: G = case x of { (Intro im) -> s (T fi) (MIt fi G s) im;} {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "Unit" as "()" con "tt" as "*" var "fi" as "F" with symbolfont var "fi'" as "F1" with symbolfont var "Times" infix rightassoc as "´" with symbolfont var "fi2" as "F2" with symbolfont var "fi1" as "F1" with symbolfont #-}