--#include "Tools.alfa" open SET use Absurd, Unit, Nat, Fin, Vec, Bool, List, Plus, Times, fst, snd, zero open Tools use OPlus, mapOPlus, sizeOPlus, eqOPlus, OTimes, mapOTimes, sizeOTimes, eqOTimes, Fam, famOPlus, famOTimes, FAM, FAMOPlus, FAMOTimes FSVec (m::Nat) :: Type = Fin m -> Set Famm (m::Nat) :: FSVec m -> Type = Fam (Fin m) FAMm (m::Nat) :: (C::FSVec m) -> Famm m C -> Type = FAM (Fin m) FSMap (m::Nat)(V::FSVec m)(W::FSVec m) :: Type = (i::Fin m) -> V i -> W i mutual Arity (m::Nat) :: Set = List (Fin m) type Seg (m::Nat) = List (Arity m) type Sig (m::Nat) = Fin m -> Seg m F (n::Nat)(fi::Sig n)(X::FSVec n) :: FSVec n = \(i::Fin n) -> OPlus (List (Fin n)) (OTimes (Fin n) X) (fi i) F1 (m::Nat)(fi::Sig m)(V::FSVec m)(W::FSVec m)(f::FSMap m V W) :: FSMap m (F m fi V) (F m fi W) = \(i::Fin m) -> mapOPlus (Arity m) (OTimes (Fin m) V) (OTimes (Fin m) W) (mapOTimes (Fin m) V W f) (fi i) FIHx (m::Nat)(fi::Sig m)(X::FSVec m)(C::Famm m X) :: Famm m (F m fi X) = \(i::Fin m) -> famOPlus (List (Fin m)) (OTimes (Fin m) X) (famOTimes (Fin m) X C) (fi i) -- T (m::Nat)(fi::Sig m) :: FSVec m -- = \(i::Fin m) -> data Intro (x::F m fi (T m fi) i) T (m::Nat)(fi::Sig m)(i::Fin m) :: Set = data Intro (x::F m fi (T m fi) i) FIH (m::Nat)(fi::Sig m) :: Famm m (T m fi) -> Famm m (F m fi (T m fi)) = FIHx m fi (T m fi) out (m::Nat)(fi::Sig m) :: FSMap m (T m fi) (F m fi (T m fi)) = \(i::Fin m) -> \(t::T m fi i) -> case t of { (Intro x) -> x;} It (m::Nat)(fi::Sig m)(C::FSVec m)(d::FSMap m (F m fi C) C) :: FSMap m (T m fi) C = \(f::Fin m) -> \(t::T m fi f) -> case t of (Intro x) -> d f (F1 m fi (T m fi) C (It m fi C d) f x) -- d f (F1 m fi (T m fi) C (It m fi C d) f (out m fi f t)) Fmap (m::Nat)(fi::Sig m)(G::FSVec m)(H::Famm m G) :: FAMm m G H -> FAMm m (F m fi G) (FIHx m fi G H) = \(f::FAMm m G H) -> \(i::Fin m) -> FAMOPlus (List (Fin m)) (OTimes (Fin m) G) (famOTimes (Fin m) G H) (FAMOTimes (Fin m) G H f) (fi i) R (m::Nat) (fi::Sig m) (C::Famm m (T m fi)) (d::(i::Fin m) -> (y::F m fi (T m fi) i) -> FIH m fi C i y -> C i (Intro@_ y)) (i::Fin m) (x::T m fi i) :: C i x = case x of { (Intro y) -> d i y (Fmap m fi (T m fi) C (R m fi C d) i y);} Nats (m::Nat) :: FSVec m = \(i::Fin m) -> Nat size_step (m::Nat)(fi::Sig m) :: FSMap m (F m fi (Nats m)) (Nats m) = \(i::Fin m) -> sizeOPlus (SET.List (Fin m)) (OTimes (Fin m) (Nats m)) (sizeOTimes (Fin m) (Nats m) zer@_ (\(a::Fin m) -> id (Nats m a))) (fi i) size (m::Nat)(fi::Sig m) :: FSMap m (T m fi) (Nats m) = It m fi (Nats m) (size_step m fi) eq_step' (m::Nat)(fi::Sig m)(Y::FSVec m) :: (i::Fin m) -> F m fi (\(i::Fin m) -> Y i -> Bool) i -> F m fi Y i -> Bool = \(i::Fin m) -> eqOPlus (List (Fin m)) (OTimes (Fin m) (\(i'::Fin m) -> Y i' -> Bool)) (OTimes (Fin m) Y) (eqOTimes (Fin m) (\(a::Fin m) -> Y a -> SET.Bool) Y (\(a::Fin m) -> id (Y a -> SET.Bool))) (fi i) eq_step (m::Nat) (fi::Sig m) (i::Fin m) (fs::F m fi (\(j::Fin m) -> T m fi j -> Bool) i) (t::T m fi i) :: Bool = case t of { (Intro x) -> eq_step' m fi (T m fi) i fs x;} eq (m::Nat)(fi::Sig m) :: (i::Fin m) -> T m fi i -> T m fi i -> Bool = It m fi (\(i::Fin m) -> T m fi i -> Bool) (eq_step m fi) -- Unused code: -- size_step_ar is not needed size_step_ar (m::Nat)(n::Arity m)(x::OTimes (Fin m) (Nats m) n) :: Nat = sizeOTimes (Fin m) (Nats m) zer@_ (\(a::Fin m) -> id (Nats m a)) n x -- eq_step_ar is not needed eq_step_ar (m::Nat)(Y::FSVec m) :: (n::Arity m) -> OTimes (Fin m) (\(i::Fin m) -> Y i -> Bool) n -> OTimes (Fin m) Y n -> Bool = eqOTimes (Fin m) (\(i::Fin m) -> Y i -> SET.Bool) Y (\(i::Fin m) -> id (Y i -> SET.Bool)) {- MIt (m::Nat) (fi::Sig m) (C::FSVec m) (s::(X::FSVec m) -> FSMap m X C -> FSMap m (F m fi X) C) :: FSMap m (T m fi) C = ? -} {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "veq" hide 2 var "fi" as "F" with symbolfont var "Plus" infix as "+" var "Times" infix leftassoc 2 as "´" with symbolfont var "fst" hide 2 var "snd" hide 2 var "FSMap" distfix3 as "=>" with symbolfont var "Famm" hide 1 var "FAMm" hide 1 #-}