Cedille

Unicode shortcuts

These can be entered in Emacs using \◌, replacing the hole with the bolded, underlined character of the mnemonic.

Mnemonic	Character
hole	●
period.	·
lambda	λ
Lambda	Λ
right, –>	➔
-⊳	➾
Pi	Π
forall	∀
star	★
Box	□
forward (?)	◂
k	𝒌
=	≃
beta	β
Rho	ρ
Fi	φ
delta	δ
why	ς
intersection	ι
mu	μ
case	σ
theta	θ
x	χ

Cedille navigation mode (Emacs)

M-s toggles Cedille navigation mode. See cedille-main-info for more commands and detailed explanations.

Command	Effect
f/b	Sibling node (forward/backward)
a/e	Sibling node (first/last)
p/n	Parent/child node (prev. visited or first)
r/R	Next/previous error
t/T	First/last error
i	Toggle node info
c	Toggle node context
s	Toggle file summary

The below are interactive commands on nodes prefixed by C-i.

Command	Effect
n/h	Normalize (head normal)
u	Reduce
e	Erase
r/R	Clear (all)

Basic syntax

Function shape	Dependent	Nondependent	Abstraction	Application
Type to type	Π x: 𝒌. 𝒌	𝒌 ➔ 𝒌	λ X: 𝒌. U	T ·U
Term to type	Π x: T. 𝒌	T ➔ 𝒌	λ x: T. U	T  e
Type to term (erased)	∀ X: 𝒌. U	⸻	Λ X: 𝒌. e	t ·U
Term to term (erased)	∀ x: T. U	T ➾ U	Λ x: T. e	t -e
Term to term	Π x: T. U	T ➔ U	λ x: T. e	t  e

Note: It appears that type applications can be left out and inferred, but not implicit term applications.

Constructs and examples

-- Declare type with kind
Unit ◂ ★
= ∀ X: ★. X ➔ X.

-- Declare term with type
unit : Unit
= Λ X. λ x. x.

-- Declare abstracted kind (pattern-matching style)
-- With the □ sort, this would be equivalent to
--   𝒌 : (Unit ➔ ★) ➔ Unit ➔ □
--   = λ F: Unit ➔ ★. λ u: Unit. F u ➔ ★.
𝒌 (F: Unit ➔ ★) (u: Unit) = F u ➔ ★.

-- Local definitions
true : ∀ X: ★. X ➔ X ➔ X
= Λ X. λ x.
  -- Erased definition
  {Y: ★ = X} - λ y: Y. x.
false : ∀ X: ★. X ➔ X ➔ X
= Λ X. λ x.
  -- Non-erased definition
  -- χ T - t asserts t has type T
  [id = χ (X ➔ X) - λ y. y] - id.

-- Trivial equality proof
refl : ∀ X: ★. ∀ x: X. {x ≃ x}
= Λ X. Λ x. β.

-- Rewriting via an equality
-- Given a goal type T and an equality p: {e ≃ e'},
-- ρ p - u will rewrite T containing e to T' containing e'
-- in place of e, proving T' with u.
-- The term e of a trivial reflexive proof {e ≃ e}
-- can be specified using β<e>.
sym : ∀ X: ★. ∀ x: X. ∀ y: X. {x ≃ y} ➔ {y ≃ x}
= Λ X. Λ x. Λ y. λ p. ρ p - β<y>.

-- Equality with explicit erasure term
-- The erasure of an equality proof β{|t|} is t;
-- since the erasure of equalities could be anything,
-- the induction hypothesis must cover all erasures.
-- Note the missing type argument of d that was inferred.
J : ∀ X: ★. ∀ x: X. ∀ P: (Π y: X. {x ≃ y} ➔ ★).
    Π d: ∀ T: ★. ∀ t: T. P x β{|t|}.
    ∀ y: X. ∀ p: {x ≃ y}. P y p
= Λ X. Λ x. Λ P. λ d. Λ y. Λ p. ρ (sym -x -y p) - d -p.

-- Subst via J with automatic motive inference
-- In the below where the θ term is, the desired type is P x ➔ P y.
-- We wish to use J to prove this, and J requires a motive P'.
-- θ<y p> then abstracts the desired type over these variables,
-- creating the motive (λ y: X. λ p: {x ≃ y}. P x ➔ P y) (p is unused),
-- then applies the motive to (J -x).
-- Without θ, this would be written as J -x ·P' (Λ T. Λ t. λ px. px) -y -p,
-- which would be a lot more tedious to write with P' explicitly stated,
-- especially since the abstracted types X and {x ≃ y}
-- syntactically need to be written out in full.
subst : ∀ X: ★. ∀ x: X. ∀ y: X. ∀ P: X ➔ ★. ∀ p: {x ≃ y}. P x ➔ P y
= Λ X. Λ x. Λ y. Λ P. Λ p. θ<y p> (J -x) (Λ T. Λ t. λ px. px) -y -p.

-- Casting via an equality
-- Given terms e: T, e', and equality p: {e ≃ e'},
-- φ p - e {|e'|} erases to e' but has type T.
Omega : {unit ≃ λ x. x x} ➾ Unit
= Λ p. [omega = φ p - unit {|λ x. x x|}] - omega omega.

-- Ex falso quodlibet
-- Given an equality p: {e ≃ e'} of Böhm-separable terms,
-- i.e. terms with distinct closed head-normal forms,
-- δ - p can be assigned any type (although it erases to λ x. x).
-- Then φ can be used to construct an X that erases to any term;
-- in the below example it erases to p, just for fun.
absurd : {true ≃ false} ➔ ∀ X: ★. X
= λ p. [void: ∀ X: ★. X = δ - p] -
Λ X. φ (void ·{void ≃ p}) - (void ·X) {|p|}.

-- Declaring a datatype
-- Parameters are elided in all recursive references.
data Acc (X: ★) (R: X ➔ X ➔ ★) : X ➔ ★ =
| acc : ∀ x: X. (∀ y: X. R y x ➔ Acc y) ➔ Acc x.

-- Case destruction with motive
-- Given a construction c, σ c @P { | C a… ➔ e } deconstructs c
-- into a constructor C and arguments a…, producing e
-- (where a… may be types ·X or implicits -x, but not parameters)
-- with optional explicit motive P abstracting over indices and target.
-- Supposing inductive I and P = λ i…. λ x. P', in Coq this would be
-- case c as x in I _… i… return P' of | C a… ➔ e end.
accessible : ∀ X: ★. ∀ R: X ➔ X ➔ ★.
             ∀ x: X. ∀ y: X. R y x ➔ Acc ·X ·R x ➔ Acc ·X ·R y
= Λ X. Λ R. Λ x. Λ y. λ r. λ accx.
σ accx @(λ x': X. λ accx': Acc ·X ·R x'. {x' ≃ x} ➔ Acc ·X ·R y) {
| acc -x accy ➔ λ p. accy -y (ρ p - r)
} β<x>.
-- Note that destructing something with an index doesn't unify
-- the index outside of the destruction and inside of it,
-- so using the convoy pattern may be necessary.

-- Well-founded induction
-- If all X are accessible and the predicate P holding for all y R x
-- means that it holds for x, then P holds for all x.
-- Given a construction c, μ f. c @P { | C a… ➔ e } is a fixed point
-- recurring on c, again with optional explicit motive P.
-- Supposing inductive I, in Coq this would be an applied fixpoint
-- (fix f (x: I) : P x := case x of | C a… ➔ e end) c
-- (omitting inductive parameters and indices).
-- Notably, the type of f abstracts over the indices as well.
wfind : ∀ X: ★. ∀ R: X ➔ X ➔ ★. (∀ x: X. Acc ·X ·R x) ➔
        ∀ P: X ➔ ★. (∀ x: X. (∀ y: X. R y x ➔ P y) ➔ P x) ➔
        ∀ x: X. P x
= Λ X. Λ R. λ accessible. Λ P. λ ih. Λ x.
μ wfind. (accessible -x) @(λ x: X. λ accx: Acc ·X ·R x. P x) {
| acc -x accy ➔ ih -x (Λ y. λ r. wfind -y (accy -y r))
}.

Generated definitions

Given a data definition (using Acc above as an example), three additional definitions are generated.

Name	Type	Description
Is/Acc	Π X: ★. Π R: X ➔ X ➔ ★. (X ➔ ★) ➔ ★	X ➔ ★ that can be used as Acc
is/Acc	∀ X: ★. ∀ R: X ➔ X ➔ ★. Is/Acc ·X ·R (Acc ·X ·R)	Trivial proof of Is/Acc
to/Acc	∀ X: ★. ∀ R: X ➔ X ➔ ★. ∀ A: X ➔ ★. Is/Acc ·X ·R ·A ➔ ∀ x: X. Acc ·X ·R x	Casts A to Acc ·X ·R

Inside of a μ f. acc @P { ... } (again using induction on an Acc ·X ·R as an example), another three definitions are generated.

Name	Type	Description
Type/f	X ➔ ★	Type of recursive arguments to f
isType/f	Is/Acc ·X ·R Type/f	Type/f is an Acc ·X ·R
f	∀ x: X . ∀ acc: Type/f x ➔ P x (to/Acc ·X ·R ·Type/f -isType/f -x acc)	Type of fixpoint

The most common use case is changing an acc : Type/f x into an Acc ·X ·R x proper with to/Acc -isType/f -x acc. (Note that type applications to definitions can be omitted when inferrable but are included above for clarity.)

Tips and tricks

• Given a falsehood void: ∀ X: ★. X, any term that erases to t can be assigned any type X by
  φ (void ·{void ≃ t}) - (void ·X) {|t|}.
• Given t: T, u: P t, and p: {t ≃ u}, an element of the intersection type ι x: T. P x is constructible despite having a propositional rather than definitional equality by
  [t, φ (ϛ p) - u {|t|}].
• When casing on an inductive e: I i with index i, the deconstruction C i' a for constructor C with argument a does not definitionally equate i to i'. To have the propositional equality available, use a convoy pattern:
  μ fix. e @P { C i a ➔ body } (doesn't type check) becomes
  μ fix. e @(λ i'. λ e'. {i ≃ i'} ➔ P i' e') { C i' a ➔ λ p. ρ p - body } β<i>.

Erasures

Erased term	Erases to
‖x‖	x
‖λ x. t‖	λ x. ‖t‖
‖t u‖	‖t‖ ‖u‖
‖Λ x. t‖	‖t‖
‖t ·U‖	‖t‖
‖t -u‖	‖t‖
‖χ T - t‖	‖t‖
‖β{|t|}‖	‖t‖
‖ρ p - t‖	‖t‖
‖φ p - u {|t|}‖	‖t‖
‖δ - p‖	λ x. x
‖[t, u]‖	‖t‖
‖t.1‖, ‖t.2‖	‖t‖

Typing rules

Sorting, kinding, typing: Γ ⊢ 𝒌 : □ — Γ ⊢ T : 𝒌 — Γ ⊢ t : T

Well-scopedness: Γ ⊢ 𝒌 — Γ ⊢ T — Γ ⊢ t

The below are only the kinding and typing rules for equality and intersection.

Γ ⊢ t : T
───────────────
Γ ⊢ χ T - t : T

Γ ⊢ t₁    Γ ⊢ t₂
────────────────
Γ ⊢ t₁ ≃ t₂ : ★

Γ ⊢ u    ‖t₁‖ ≅ ‖t₂‖
────────────────────
Γ ⊢ β{|u|} : t₁ ≃ t₂

Γ ⊢ p : {t₁ ≃ t₂}    Γ ⊢ u : T[x ↦ t₂]
──────────────────────────────────────
Γ ⊢ ρ p - u : T[x ↦ t₁]

Γ ⊢ p : {t₁ ≃ t₂}    Γ ⊢ t₁ : T
───────────────────────────────
Γ ⊢ φ p - t₁ {|t₂|} : T

Γ ⊢ p : {t₁ ≃ t₂}    ‖t₁‖ ≇ ‖t₂‖
────────────────────────────────
Γ ⊢ δ - p : T

Γ ⊢ T : ★    Γ, x: T ⊢ U : ★
────────────────────────────
Γ ⊢ ι x: T. U : ★

Γ ⊢ t : T    Γ ⊢ u : U[x ↦ t]    ‖t‖ ≅ ‖u‖
──────────────────────────────────────────
Γ ⊢ [t, u] : ι x: T. U

Γ ⊢ t : ι x: T. U
───────────────────────────────────
Γ ⊢ t.1 : T    Γ ⊢ t.2 : U[x ↦ t.1]