Skip to content

Instantly share code, notes, and snippets.

@Icelandjack

Icelandjack/nary_composition.agda

Last active October 11, 2021 12:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Icelandjack/2eb99db6a1ab904b709571f1e9cd36b4 to your computer and use it in GitHub Desktop.
Save Icelandjack/2eb99db6a1ab904b709571f1e9cd36b4 to your computer and use it in GitHub Desktop.
Download ZIP
Dependent polyvariadic mixfix function composition in Agda
Raw
nary_composition.agda
infixr 80 _◦_
_◦_ : forall {l1 l2 l3 : Level }
{A : -> Set l1}
{B : A -> Set l2}
{C : (a : A) -> B a -> Set l3}
(g : {a : A} -> (b : B a) -> C a b )
(f : (a : A) -> B a)
-> (a : A) -> C a (f a)
g ◦ f = \a -> g (f a)
infix 100 _◦
_◦ : forall {l1 l2 l3 : Level }
{A : Set l1}
{B : A -> Set l2}
{C : (a : A) -> B a -> Set l3}
(g : {a : A} -> (b : B a) -> C a b )
(f : (a : A) -> B a)
-> (a : A) -> C a (f a)
_◦ = _◦_
phi : N -> N -> N
phi = succ ◦ ◦ _+_
_ : phi 2 3 = 6
_ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment