namespace latin:/❚

fixmeta ur:?LF❚

theory SimpleFunctionTypes =
  include ?Types❙
  simpfun : tp ⟶ tp ⟶ tp❘# 1 %R→ 2 prec 50❙
  test = [a:tp] a → a → a❙
❚

theory DependentFunctionTypes =
  include ?TypedTerms❙
  depfun : {A} (tm A ⟶ tp) ⟶ tp❘# Π 2 prec 40❙
  realize ?SimpleFunctionTypes❙
  simpfun = [A,B] Π [x: tm A] B❙
❚

theory SoftDependentFunctionTypes =
  include ?SoftTypedTerms❙
  softfun : tp ⟶ (term ⟶ tp) ⟶ tp❘# Π 1 2 prec 40❙
❚

theory SimpleFunctions =
  include ?SimpleFunctionTypes❙
  include ?TypedEquality❙
  simplambda: {A,B} (tm A ⟶ tm B) ⟶ tm A → B❘# λ 3 prec 40❙
  simpapply: {A,B} tm A → B ⟶ tm A ⟶ tm B❘# 3 @ 4 prec 50❙
  simpbeta : {A,B,F: tm A ⟶ tm B, X} ⊦ (λ F) @ X ≐ F X❙

  // should be an extra notation for simpapply❙
  apply1 : {a,b} tm a→b ⟶ (tm a ⟶ tm b)❘
         = [a,b,f] [x] f@x❘# %%prefix 2 1❙
  applyTo : {a,b} tm a ⟶ tm (a→b)→b❘= [a,b,x] λ[f]f@x❘# applyTo 3❙
❚

theory DependentFunctions =
  include ?DependentFunctionTypes❙
  include ?TypedEquality❙
  deplambda: {A,B} ({x: tm A} tm B x) ⟶ tm Π B❘# λ 3 prec 40❙
  depapply: {A,B} tm Π B ⟶ {x: tm A} tm B x ❘# 3 @ 4 prec 50❙
  depbeta : {A,B,F:{x:tm A} tm B x, X} ⊦ (λ F) @ X ≐ F X❙
  
  // realize ?SimpleFunctions❙
  // simplambda = [A,B,F] λ[x:tm A] F x❙
  // simpapply = [A,B,F,X] F @ X❙
  // simpbeta = [A,B,F,X] depbeta❙
❚

theory SoftTypedFunctions =
  include ?Terms❙
  include ?SoftTypedEquality❙
  lambda: (term ⟶ term) ⟶ term❘# λ 1 prec 40❙
  apply : term ⟶ term ⟶ term❘# 1 @ 2 prec 50❙
  beta  : {F,X} ⊦ (λ F) @ X ≐ F X❙
❚

theory SoftTypedSimpleFunctions =
  include ?SoftTypedTerms❙
  include ?SoftTypedFunctions❙
  include ?SimpleFunctionTypes❙
  fun_typing : {A,B,F} ({x} ⊦ x⦂A ⟶ ⊦ (F x)⦂B) ⟶ ⊦ λ F ⦂ A → B❙
❚

theory SoftTypedDependentFunctions =
  include ?SoftTypedTerms❙
  include ?SoftTypedFunctions❙
  include ?SoftDependentFunctionTypes❙
  fun_typing : {A,B,F} ({x} ⊦ x⦂A ⟶ ⊦ (F x)⦂(B x)) ⟶ ⊦ λ F ⦂ Π A B❙
❚

theory SimpleFunctionsEta =
  include ?SimpleFunctions❙
  eta: {A,B,F:tm A → B} ⊦ (λ[x] F @ x) ≐ F❙
❚

theory DependentFunctionsEta =
  include ?DependentFunctions❙
  eta: {A,B, F:tm Π[x:tm A] B x} ⊦ (λ[x] F @ x) ≐ F❙
❚

theory SoftTypedFunctionsEta =
  include ?SoftTypedFunctions❙
  eta: {F} ⊦ (λ[x] F @ x) ≐ F❙
❚

theory SimpleFunctionsExtensionality =
  include ?SimpleFunctions❙
  exten: {A,B,F,G:tm A → B} ({x} ⊦ F@x ≐ G@x) ⟶ ⊦ F≐G❙
❚

theory DependentFunctionsExtensionality =
  include ?DependentFunctions❙
  exten: {A,B, F,G:tm Π[x:tm A] B x} ({x} ⊦ F@x ≐ G@x) ⟶ ⊦ F≐G❙
❚

theory SofttypedFunctionsExtensionality =
  include ?SoftTypedFunctions❙
  eta: {F,G} ({x} ⊦ F@x ≐ G@x) ⟶ ⊦ F≐G❙
❚