Core.prelude

id : {A : π•Œ} (x : A) β†’ A
id = Ξ»A x. x

infixr 1 ∘
∘ : {A B C : π•Œ} (g : B β†’ C) (f : A β†’ B) β†’ A β†’ C
(∘) = λA B C g f x. g (f x)

idP : {A : Ξ©} (x : A) β†’ A
idP = Ξ»A x. x

const : {A B : π•Œ} (x : A) (y : B) β†’ A
const = Ξ»A B x y. x

constP : {A B : Ξ©} (x : A) (y : B) β†’ A
constP = Ξ»A B x y. x

-- Function extensionality β€” a theorem here, not an axiom: reflect the
-- pointwise hypothesis under the binder and the sides are equal by
-- ΞΎ and Ξ· (funext-via-reflection, NovaFoundation's Ξ½ SUBSUMPTION note).
funext : {A : π•Œ} {B : A β†’ π•Œ} {f g : (x : A) β†’ B x} β†’ ((x : A) β†’ f x ≑ g x) β†’ f ≑ g using (pi.eta)
funext = Ξ»A B f g h. ⋆