fact: Definition lambda_calculus_data : UU := ∑ (L : nat → hSet) (var : ∏ n, stn n → L n) (app : ∏ n, L n → L n → L n) (abs : ∏ n, L (S n) → L n) (subst : ∏ m n, L m → (stn m → L n) → L n) (inflate := (λ _ l, subst _ _ l (λ i, (var _ (stnweq (inl i))))) : ∏ n, L n → L (S n)) (subst_var : ∏ m n i (f : stn m → L n), subst _ _ (var _ i) f = f i) (subst_app : ∏ m n l l' (f : stn m → L n), subst _ _ (app _ l l') f = app _ (subst _ _ l f) (subst _ _ l' f)) (subst_abs : ∏ m n l (f : stn m → L n), subst _ _ (abs _ l) f = abs _ (subst _ _ l (extend_tuple (λ i, inflate _ (f i)) (var _ (stnweq (inr tt)))))) (subst_subst : ∏ l m n t (g : stn l → L m) (f : stn m → L n), subst _ _ (subst _ _ t g) f = subst _ _ t (λ i, subst _ _ (g i) f)) (beta : ∏ n (f : L (S n)) g, app _ (abs _ f) g = subst _ _ f (extend_tuple (var _) g)), (∏ (A : ∏ n l, hSet) (f_var : ∏ n i, A n (var n i)) (f_app : ∏ n l l', A _ l → A _ l' → A _ (app n l l')) (f_abs : ∏ n l, A _ l → A _ (abs n l)) (f_subst : ∏ m n l f, A _ l → (∏ i, A _ (f i)) → A _ (subst m n l f)) (f_inflate := (λ n _ al, f_subst _ _ _ _ al (λ i, (f_var _ (stnweq (inl i))))) : ∏ n (l : L n), A n l → A (S n) (inflate _ l)) (f_subst_var : ∏ m n i f af, PathOver (Y := A n) (subst_var m n i f) (f_subst _ _ _ _ (f_var _ i) af) (af i)) (f_subst_app : ∏ m n l al l' al' f af, PathOver (Y := A n) (subst_app m n l l' f) (f_subst _ _ _ _ (f_app _ _ _ al al') af) (f_app _ _ _ (f_subst _ _ _ _ al af) (f_subst _ _ _ _ al' af))) (f_subst_abs : ∏ m n l al f af, PathOver (Y := A n) (subst_abs m n l f) (f_subst _ _ _ _ (f_abs _ _ al) af) (f_abs _ _ (f_subst _ _ _ _ al (extend_tuple_dep (A := A (S n)) (λ i, f_inflate _ _ (af i)) (f_var _ (stnweq (inr tt))))))) (f_subst_subst : ∏ l m n t a g ag f af, PathOver (Y := A n) (subst_subst l m n t g f) (f_subst _ _ _ _ (f_subst _ _ _ _ a ag) af) (f_subst _ _ _ _ a (λ i, f_subst _ _ _ _ (ag i) af))) (f_beta : ∏ n f af g ag, PathOver (Y := A n) (beta n f g) (f_app _ _ _ (f_abs _ _ af) ag) (f_subst _ _ _ _ af (extend_tuple_dep (A := A n) (f_var _) ag))) , (∏ n l, A n l) ).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples