All your base categories are belong to us
A syntactic model of presheaves in type theory

Pierre-Marie PédrotINRIA, Gallinette team

MSFP 2020
31st August 2020

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

1 / 54

It’s Time to CIC Ass
CIC, the Calculus of Inductive Constructions.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

2 / 54

It’s Time to CIC Ass
CIC, the Calculus of Inductive Constructions.
CIC, a very fancy intuitionistic logical system.
Not just higher-order logic, not just first-order logic
First class notion of computation and crazy inductive types

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

2 / 54

It’s Time to CIC Ass
CIC, the Calculus of Inductive Constructions.
CIC, a very fancy intuitionistic logical system.
Not just higher-order logic, not just first-order logic
First class notion of computation and crazy inductive types
CIC, a very powerful functional programming language.
Finest types to describe your programs
No clear phase separation between runtime and compile timeP.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

2 / 54

It’s Time to CIC Ass
CIC, the Calculus of Inductive Constructions.
CIC, a very fancy intuitionistic logical system.
Not just higher-order logic, not just first-order logic
First class notion of computation and crazy inductive types
CIC, a very powerful functional programming language.
Finest types to describe your programs
No clear phase separation between runtime and compile time

The Pinnacle of the Curry-Howard correspondence

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

2 / 54

It’s Time to CIC Ass
CIC, the Calculus of Inductive Constructions.
CIC, a very fancy intuitionistic logical system.
Not just higher-order logic, not just first-order logic
First class notion of computation and crazy inductive types
CIC, a very powerful functional programming language.
Finest types to describe your programs
No clear phase separation between runtime and compile time

The Pinnacle of the Curry-Howard correspondence

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

2 / 54

The Good Properties™
Consistency There is no proof of False.
Implementability Type-checking is decidable.
Canonicity Closed integers are indeed integers, i.e`M:N

implies

M ≡ S ... SO

Assuming we have a notion of reduction compatible with conversion:
Normalization Reduction is normalizing
Subject reduction Reduction is compatible with typing

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

3 / 54

The Good Properties™
Consistency There is no proof of False.
Implementability Type-checking is decidable.
Canonicity Closed integers are indeed integers, i.e`M:N

implies

M ≡ S ... SO

Assuming we have a notion of reduction compatible with conversion:
Normalization Reduction is normalizing
Subject reduction Reduction is compatible with typing

Some of these properties are interdependent

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

3 / 54Extending Coq in Three Easy Steps
Our mission
To boldly extend the logical / computational expressivity of CIC

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

4 / 54Extending Coq in Three Easy Steps
Our mission
To boldly extend the logical / computational expressivity of CIC⇝ we need to design models for that.
⇝ and ensure they satisfy The Good Properties™.
Today we will focus on a specific family of models...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

4 / 54Extending Coq in Three Easy Steps
Our mission
To boldly extend the logical / computational expressivity of CIC⇝ we need to design models for that.
⇝ and ensure they satisfy The Good Properties™.
Today we will focus on a specific family of models...

Presheaves!
Proof-relevant Kripke semantics / Intuitionistic Forcing
Bread and Butter of Model Construction
They Are Everywhere: Cubical, Modal, Guarded, NbE, ...
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

4 / 54

I Herd U Liek Murphims

Definition
Let P be a category. A presheaf over P is just a functor Pop → Set.
(In what follows we will fix the base category P once and for all.)P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

5 / 54

I Herd U Liek Murphims

Definition
Let P be a category. A presheaf over P is just a functor Pop → Set.
(In what follows we will fix the base category P once and for all.)TheoremPresheaves with nat. transformations as morphisms form a category Psh(P).

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

5 / 54

I Herd U Liek Murphims

Definition
Let P be a category. A presheaf over P is just a functor Pop → Set.
(In what follows we will fix the base category P once and for all.)TheoremPresheaves with nat. transformations as morphisms form a category Psh(P).

Actually Psh(P) is even a topos!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

5 / 54

I Herd U Liek Murphims

Definition
Let P be a category. A presheaf over P is just a functor Pop → Set.
(In what follows we will fix the base category P once and for all.)TheoremPresheaves with nat. transformations as morphisms form a category Psh(P).

Actually Psh(P) is even a topos!
Bear with me, we will handwave through this in the next slides.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

5 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

6 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Objects: A presheaf (A, θA ) is given by
A family of P-indexed sets Ap : Set
A family of “restriction morphisms” (a.k.a. monotonicity)θA : Π{p, q ∈ P} (α ∈ P(q, p)). Ap → Aq

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

6 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Objects: A presheaf (A, θA ) is given by
A family of P-indexed sets Ap : Set
A family of “restriction morphisms” (a.k.a. monotonicity)θA : Π{p, q ∈ P} (α ∈ P(q, p)). Ap → Aq

“θA α x lowers its argument x along α ∈ P(q, p)”

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

6 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Objects: A presheaf (A, θA ) is given by
A family of P-indexed sets Ap : Set
A family of “restriction morphisms” (a.k.a. monotonicity)θA : Π{p, q ∈ P} (α ∈ P(q, p)). Ap → Aq

“θA α x lowers its argument x along α ∈ P(q, p)”s.t. given x ∈ Ap , α ∈ P(q, p) and β ∈ P(r, q):θA idp x ≡ x

P.-M. Pédrot (INRIA, Gallinette team)θA (β ◦ α) x ≡ θA β (θA α x)

All your base categories are belong to us

31/08/2020

6 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Objects: A presheaf (A, θA ) is given by
A family of P-indexed sets Ap : Set
A family of “restriction morphisms” (a.k.a. monotonicity)θA : Π{p, q ∈ P} (α ∈ P(q, p)). Ap → Aq

“θA α x lowers its argument x along α ∈ P(q, p)”s.t. given x ∈ Ap , α ∈ P(q, p) and β ∈ P(r, q):θA idp x ≡ xθA (β ◦ α) x ≡ θA β (θA α x)

“Lowering is compatible with the structure of P”
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

6 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

7 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Morphisms: A morphism from (A, θA ) to (B, θB ) is given by
A family of P-indexed functions fp : Ap → Bp
which is natural, i.e. given x ∈ Ap and α ∈ P(q, p)
θB α (fp x) ≡ fq (θA α x)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

7 / 54

All Your Base Category Are Belong to Us
What is Psh(P)?
Morphisms: A morphism from (A, θA ) to (B, θB ) is given by
A family of P-indexed functions fp : Ap → Bp
which is natural, i.e. given x ∈ Ap and α ∈ P(q, p)
θB α (fp x) ≡ fq (θA α x)

“f is compatible with restriction”
Ap
θA α



Aq
P.-M. Pédrot (INRIA, Gallinette team)

fp

fq

/ Bp


θB α

/ Bq

All your base categories are belong to us

31/08/2020

7 / 54

The Wise Speak Only of What They Know
Psh(P) is a topos.

“Speak, friend, and pullback.”

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

8 / 54

The Wise Speak Only of What They Know
Psh(P) is a topos.

“Speak, friend, and pullback.”

Who cares?

Presheaves actually form a model of CIC.
` A : □ ⇝ [[A]] ∈ Psh(P)P.-M. Pédrot (INRIA, Gallinette team)` M : A ⇝ [M] ∈ Nat(1, [[A]])All your base categories are belong to us

31/08/2020

8 / 54

The Wise Speak Only of What They Know
Psh(P) is a topos.

“Speak, friend, and pullback.”

Who cares?

Presheaves actually form a model of CIC.
` A : □ ⇝ [[A]] ∈ Psh(P)` M : A ⇝ [M] ∈ Nat(1, [[A]])Yet another set-theoretical model!
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

8 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

P.-M. Pédrot (INRIA, Gallinette team)☺

All your base categories are belong to us

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

☺

Canonicity Closed integers are integers... are they?
`M:N

P.-M. Pédrot (INRIA, Gallinette team)“(C)ZF-implies” M ≡ S . . . S O

All your base categories are belong to us😕

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

☺

Canonicity Closed integers are integers... are they?
`M:N“(C)ZF-implies” M ≡ S . . . S O

Implementability Type-checking is not decidable.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us😕

☹

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

☺

Canonicity Closed integers are integers... are they?
`M:N“(C)ZF-implies” M ≡ S . . . S O

Implementability Type-checking is not decidable.

☹

Reduction Never heard of that. What’s syntax already?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us😕
😱

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

☺

Canonicity Closed integers are integers... are they?
`M:N“(C)ZF-implies” M ≡ S . . . S O

Implementability Type-checking is not decidable.

😕

☹

Reduction Never heard of that. What’s syntax already?

😱

⇝ Exeunt Normalization and Subject reduction.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

9 / 54ZF Set Up Us The Bomb
Let’s have a look at The Good Properties™ we long for.
Consistency There is no proof of False.

☺

Canonicity Closed integers are integers... are they?
`M:N“(C)ZF-implies” M ≡ S . . . S O

Implementability Type-checking is not decidable.

😕

☹

Reduction Never heard of that. What’s syntax already?

😱

⇝ Exeunt Normalization and Subject reduction.
Phenomenological Law

Set-theoretical models suck.
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

9 / 54

Down With Semantics

Syntactic Models

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

10 / 54

The Bleak Truth

What is a model?
Takes syntax as input.
Interprets it into some low-level language.
Must preserve the meaning of the source.
Refines the behaviour of under-specified structures.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

11 / 54

The Bleak Truth

What is a model?
Takes syntax as input.
Interprets it into some low-level language.
Must preserve the meaning of the source.
Refines the behaviour of under-specified structures.
This looks suspiciously familiar...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

11 / 54

The Bleak Truth

What is a model?
Takes syntax as input.
Interprets it into some low-level language.
Must preserve the meaning of the source.
Refines the behaviour of under-specified structures.
This looks suspiciously familiar...

“This is a compiler!”
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

11 / 54

On Curry-Howard Poetry
General models are more like interpreters.
No separation between target vs. host languages`S M : A

P.-M. Pédrot (INRIA, Gallinette team)host−→ ⊨M A“a blob”

All your base categories are belong to us

31/08/2020

12 / 54

On Curry-Howard Poetry
General models are more like interpreters.
No separation between target vs. host languages`S M : A

host−→ ⊨M A“a blob”

Syntactic models are proper compilers.
Target is unrelated to the host language.
`S M : A

P.-M. Pédrot (INRIA, Gallinette team)host−→ `T [M ] : [[A]]All your base categories are belong to us“an AST”

31/08/2020

12 / 54

On Curry-Howard Poetry
General models are more like interpreters.
No separation between target vs. host languages`S M : A

host−→ ⊨M A“a blob”

Syntactic models are proper compilers.
Target is unrelated to the host language.
`S M : A

host−→ `T [M ] : [[A]]“an AST”

We will be interested in instances where S, T are type theories.
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

12 / 54

Why Syntactic Models?
compilation`S M : A

P.-M. Pédrot (INRIA, Gallinette team)

implies

All your base categories are belong to us`T [M] : [[A]]31/08/2020

13 / 54

Why Syntactic Models?
compilation`S M : A

implies`T [M] : [[A]]Obviously, that’s subtle.
The translation [·] must preserve typing (not easy)
In particular, it must preserve conversion (even worse)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

13 / 54

Why Syntactic Models?
compilation`S M : A

implies`T [M] : [[A]]Obviously, that’s subtle.
The translation [·] must preserve typing (not easy)
In particular, it must preserve conversion (even worse)
Yet, a lot of nice consequences.
Does not require non-type-theoretical foundations (monism)
If T is CIC, can be implemented in Coq (software monism)
Inherit properties from CIC: computationality, decidability, implementation...
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

13 / 54

“Is it possible to see the presheaf
construction as a syntactic model?”Sheaf
French Coat of Arms

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

14 / 54

Persevere Diabolicum
Why the hell am I talking about syntactic presheaves today?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

15 / 54

Persevere Diabolicum
Why the hell am I talking about syntactic presheaves today?

2012

2016

Extending Type
Theory with
Forcing

The Deﬁnitional
Side of the Forcing

Russian Constructivism
in a Prefascist Theory

FAIL

FAIL

YAY?

(LICS, Jaber,
Tabareau, Sozeau)

P.-M. Pédrot (INRIA, Gallinette team)(LICS, Jaber,
Lewertowski, Pédrot,
Tabareau, Sozeau)

2020

All your base categories are belong to us(LICS, Pédrot)

31/08/2020

15 / 54

Persevere Diabolicum
Why the hell am I talking about syntactic presheaves today?

2012

2016

Extending Type
Theory with
Forcing

The Deﬁnitional
Side of the Forcing

Russian Constructivism
in a Prefascist Theory

FAIL

FAIL

YAY?

(LICS, Jaber,
Tabareau, Sozeau)(LICS, Jaber,
Lewertowski, Pédrot,
Tabareau, Sozeau)

2020(LICS, Pédrot)

It is the journey, not the destination
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

15 / 54(We were warned.)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

16 / 54

Syntactic Presheaves, 2012 Edition“A presheaf is just a functor Pop → Set.”

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

17 / 54

Syntactic Presheaves, 2012 Edition“A presheaf is just a functor Pop → Set.”“Hold my beer!”P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

17 / 54

Syntactic Presheaves, 2012 Edition“A presheaf is just a functor Pop → Set.”“Hold my beer!”

Replace Set everywhere with CIC.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

17 / 54

Syntactic Presheaves, 2012 Edition“A presheaf is just a functor Pop → Set.”“Hold my beer!”

Replace Set everywhere with CIC.

What could possibly go wrong?
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

17 / 54

Close Encounters of the Third Type
Replace Set everywhere with CIC.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

18 / 54

Close Encounters of the Third Type
Replace Set everywhere with CIC.


P:□








≤:
P
→
P
→
□


id : Πp. p ≤ p
Cat : □:=
◦ : Πp q r. p ≤ q → q ≤ r → p ≤ r 






eqn : . . . ; A:P→□
θA : Π(p q : P) (α : q ≤ p). Ap → Aq
Psh : □:=

eqn : . . . ;{}el : Π(p : P). A p
El (A, θA , e) : □ :=eqn : . . . ;P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

18 / 54

Close Encounters of the Third Type
Replace Set everywhere with CIC.


P:□








≤:
P
→
P
→
□


id : Πp. p ≤ p
Cat : □:=
◦ : Πp q r. p ≤ q → q ≤ r → p ≤ r 






eqn : . . . ; A:P→□
θA : Π(p q : P) (α : q ≤ p). Ap → Aq
Psh : □:=

eqn : . . . ;{}el : Π(p : P). A p
El (A, θA , e) : □ :=eqn : . . . ;And voilá, the Great Typification is an utter success!
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

18 / 54

Equality is Too Serious a Matter
This almost works...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

19 / 54

Equality is Too Serious a Matter
This almost works...
... except that equations are propositional !!!
{El (A, θA , e) : □ :=el : Π(p : P). A p
eqn : . . . ;}`CIC M ≡ N −6 → ` [M ] ≡ [N]`CIC M ≡ N −→ ` e : [M ] = [N]P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

19 / 54

Equality is Too Serious a Matter
This almost works...
... except that equations are propositional !!!
{El (A, θA , e) : □ :=el : Π(p : P). A p
eqn : . . . ;}`CIC M ≡ N −6 → ` [M ] ≡ [N]`CIC M ≡ N −→ ` e : [M ] = [N]😱 You need to introduce rewriting everywhere😱

“The Coherence Hell”

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

19 / 54

Equality is Too Serious a Matter
This almost works...
... except that equations are propositional !!!
{El (A, θA , e) : □ :=el : Π(p : P). A p
eqn : . . . ;}`CIC M ≡ N −6 → ` [M ] ≡ [N]`CIC M ≡ N −→ ` e : [M ] = [N]😱 You need to introduce rewriting everywhere😱

“The Coherence Hell”

😱 Thus the target theory must be EXTENSIONAL 😱
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

19 / 54

That Was Not My Intension
Extensional Type Theory (ETT) is defined by Santa Claus conversion.
Γ`e:M=NΓ`M≡NP.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

20 / 54

That Was Not My Intension
Extensional Type Theory (ETT) is defined by Santa Claus conversion.
Γ`e:M=NΓ`M≡N
Arguably better than ZFC (“constructive”)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

20 / 54

That Was Not My Intension
Extensional Type Theory (ETT) is defined by Santa Claus conversion.
Γ`e:M=NΓ`M≡N
Arguably better than ZFC (“constructive”)... but undecidable type checking... no computation, e.g. β-reduction is undecidable
See Théo Winterhalter’s soon to be defended PhD for more horrors

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

20 / 54

That Was Not My Intension
Extensional Type Theory (ETT) is defined by Santa Claus conversion.
Γ`e:M=NΓ`M≡N
Arguably better than ZFC (“constructive”)... but undecidable type checking... no computation, e.g. β-reduction is undecidable
See Théo Winterhalter’s soon to be defended PhD for more horrors
No True Scotsman
Syntactic models into ETT are not really syntactic models† .

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

20 / 54

That Was Not My Intension
Extensional Type Theory (ETT) is defined by Santa Claus conversion.
Γ`e:M=NΓ`M≡N
Arguably better than ZFC (“constructive”)... but undecidable type checking... no computation, e.g. β-reduction is undecidable
See Théo Winterhalter’s soon to be defended PhD for more horrors
No True Scotsman
Syntactic models into ETT are not really syntactic models† .
(†) To be more precise, I believe that ETT is not really a type theory.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

20 / 54

(Make conversion great again, and break everything else.)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

21 / 54

Squaring the Circle(Me to the authors of the 2012 paper, some time before defending PhD.)— You people are doing it wrong. It cannot work!
— Why?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

22 / 54

Squaring the Circle(Me to the authors of the 2012 paper, some time before defending PhD.)— You people are doing it wrong. It cannot work!
— Why?

— Because presheaves are call-by-value!
... and you’re trying to intepret a call-by-name language!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

22 / 54

Squaring the Circle(Me to the authors of the 2012 paper, some time before defending PhD.)— You people are doing it wrong. It cannot work!
— Why?

— Because presheaves are call-by-value!
... and you’re trying to intepret a call-by-name language!

— What on earth does that even mean?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

22 / 54

This is the Left Adjoint, Right?
CBPV is a nice framework to study effects.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

23 / 54

This is the Left Adjoint, Right?
CBPV is a nice framework to study effects.
... but I don’t have enough time to present it here.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

23 / 54

This is the Left Adjoint, Right?
CBPV is a nice framework to study effects.
... but I don’t have enough time to present it here.

Theorem
Kripke models factorize through CBPV.
A
value type7→ [[A]]v : Fun(Pop , Set)
X computation type 7→ [[X]]c : |P| → Set

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

23 / 54

This is the Left Adjoint, Right?
CBPV is a nice framework to study effects.
... but I don’t have enough time to present it here.

Theorem
Kripke models factorize through CBPV.
A
value type7→ [[A]]v : Fun(Pop , Set)
X computation type 7→ [[X]]c : |P| → Set[[U X]]vp := Π(q : P)(α : q ≤ p). [[X]]cq(free functoriality)

θ[[U X]]v (α : q ≤ p)(x : [[U X]]vp ) := λ(r : P)(β : r ≤ q). x r (α ◦ β)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

23 / 54

More Than One Way to Do It
Theorem
Kripke models factorize through CBPV.
Canonical embeddings of λ-calculus into CBPV:
CBN
CBV(σ → τ )N :=U σN → τ N(a computation type)V(σ → τ ) := U (σ V → F τ V )(a value type)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

24 / 54

More Than One Way to Do It
Theorem
Kripke models factorize through CBPV.
Canonical embeddings of λ-calculus into CBPV:
CBN
CBV(σ → τ )N :=U σN → τ N(a computation type)V(σ → τ ) := U (σ V → F τ V )(a value type)Thus, composing the CBV embedding with the “Kripke” interpretation:[[(σ → τ )V ]]vp := Π(q : P)(α : q ≤ p). [[σ V ]]vq → [[τ V ]]vq

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

24 / 54

More Than One Way to Do It
Theorem
Kripke models factorize through CBPV.
Canonical embeddings of λ-calculus into CBPV:
CBN
CBV(σ → τ )N :=U σN → τ N(a computation type)V(σ → τ ) := U (σ V → F τ V )(a value type)Thus, composing the CBV embedding with the “Kripke” interpretation:[[(σ → τ )V ]]vp := Π(q : P)(α : q ≤ p). [[σ V ]]vq → [[τ V ]]vq

This is the presheaf interpretation of arrows! (up to naturality)∗∗P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

24 / 54

Le Clash
Presheaves are call-by-value!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

25 / 54

Le Clash
Presheaves are call-by-value!
In particular, they only satisfy the CBV equational theory generated by(λx. t) V ≡βv t{x := V}becauset ≡βv u−→P.-M. Pédrot (INRIA, Gallinette team)tV ≡CBPV uV−→

All your base categories are belong to us[tV ]p ≡T [uV ]p

31/08/2020

25 / 54

Le Clash
Presheaves are call-by-value!
In particular, they only satisfy the CBV equational theory generated by(λx. t) V ≡βv t{x := V}becauset ≡βv u−→tV ≡CBPV uV−→[tV ]p ≡T [uV ]pType theory is call-by-name!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

25 / 54

Le Clash
Presheaves are call-by-value!
In particular, they only satisfy the CBV equational theory generated by(λx. t) V ≡βv t{x := V}becauset ≡βv u−→tV ≡CBPV uV[tV ]p ≡T [uV ]p−→Type theory is call-by-name!
Γ`M:BΓ ` A ≡β B

Γ`M:A

P.-M. Pédrot (INRIA, Gallinette team)(Conv)All your base categories are belong to us

31/08/2020

25 / 54

Le Clash
Presheaves are call-by-value!
In particular, they only satisfy the CBV equational theory generated by(λx. t) V ≡βv t{x := V}becauset ≡βv u−→tV ≡CBPV uV[tV ]p ≡T [uV ]p−→Type theory is call-by-name!
Γ`M:BΓ ` A ≡β B

Γ`M:A(Conv)

Folklore

Call-by-name is not call-by-value!
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

25 / 54

If There is No Solution, There is No Problem
Easy solution! Pick the CBN decomposition instead.
[[(σ → τ )N ]]cp := (Π(q : P)(α : q ≤ p). [[σ N ]]cq ) → [[τ N ]]cp

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

26 / 54

If There is No Solution, There is No Problem
Easy solution! Pick the CBN decomposition instead.
[[(σ → τ )N ]]cp := (Π(q : P)(α : q ≤ p). [[σ N ]]cq ) → [[τ N ]]cp

This adapts straightforwardly to the dependently-typed setting.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

26 / 54

If There is No Solution, There is No Problem
Easy solution! Pick the CBN decomposition instead.
[[(σ → τ )N ]]cp := (Π(q : P)(α : q ≤ p). [[σ N ]]cq ) → [[τ N ]]cp

This adapts straightforwardly to the dependently-typed setting.
Theorem (Jaber & al. 2016)
There is a syntactic “presheaf model” of CCω into CIC.
where CCω is CIC without inductive types.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

26 / 54

If There is No Solution, There is No Problem
Easy solution! Pick the CBN decomposition instead.
[[(σ → τ )N ]]cp := (Π(q : P)(α : q ≤ p). [[σ N ]]cq ) → [[τ N ]]cp

This adapts straightforwardly to the dependently-typed setting.
Theorem (Jaber & al. 2016)
There is a syntactic “presheaf model” of CCω into CIC.
where CCω is CIC without inductive types.

`CCω A : □ −→ p : P `CIC [A]p : Π(q : P)(α : q ≤ p). □`CCω M : A −→ p : P `CIC [M]p : [A]p p idp`CCω M ≡ N −→ p : P `CIC [M]p ≡ [N ]p
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

26 / 54

Robbing Peter to Pay Paul
“What about inductive types?”

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

27 / 54

Robbing Peter to Pay Paul
“What about inductive types?”
The model disproves induction principles...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

27 / 54

Robbing Peter to Pay Paul
“What about inductive types?”
The model disproves induction principles...
Not A Suprise

The Kripke translation introduces an effect! (a monotonic reader)

The Proverbial PaulCBPV Folklore
In effectful CBV, functions are not functions. (no substitution)
In effectful CBN, inductive types are not inductive types. (no dep. elim.)
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

27 / 54

Conclusion of the Episode II

Good News

This is one of the first reasonable examples of dependent effects.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

28 / 54

Conclusion of the Episode II

Good News

This is one of the first reasonable examples of dependent effects.
Bad News

We still don’t have a syntactic presheaf model.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

28 / 54

Interlude

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

29 / 54

Interlude

In the meantime we worked quite a bit on effectful type theories
Weaning translation
Baclofen Type Theory
Exceptional Type Theory...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

30 / 54

Interlude

In the meantime we worked quite a bit on effectful type theories
Weaning translation
Baclofen Type Theory
Exceptional Type Theory...

This helped us understand what we first missed!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

30 / 54

Values Are Not What They Once Were
Categorical presheaves form a model of the whole λ-calculus.
... in particular, it does interpret full β-conversion (although extensionally).

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

31 / 54

Values Are Not What They Once Were
Categorical presheaves form a model of the whole λ-calculus.
... in particular, it does interpret full β-conversion (although extensionally).
This is because of the naturality requirement on functions.

[[A]]q[[A → B]]p:=f : Π(q ≤ p). [[A]]q → [[B]]q

P.-M. Pédrot (INRIA, Gallinette team)s.t.

All your base categories are belong to us

θA β

fq α

/ [[B]]qθB β fr (α◦β) / [[B]]r[[A]]r

31/08/2020

31 / 54

Values Are Not What They Once Were
Categorical presheaves form a model of the whole λ-calculus.
... in particular, it does interpret full β-conversion (although extensionally).
This is because of the naturality requirement on functions.

[[A]]q[[A → B]]p:=f : Π(q ≤ p). [[A]]q → [[B]]q

s.t.

fq α

θA β

/ [[B]]qθB β fr (α◦β) / [[B]]r[[A]]rWe do not have an equivalent in our CBN interpretation
Isn’t this some ad-hoc trick?
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

31 / 54

Completely Unrelated Slide
Consider an effectful CBV λ-calculus.

Definition (Führmann ’99)
A term t : A is said to be thunkable if it satisfies the equation
let x := t in λ(). x

P.-M. Pédrot (INRIA, Gallinette team)≡λ(). tAll your base categories are belong to us

31/08/2020

32 / 54

Completely Unrelated Slide
Consider an effectful CBV λ-calculus.

Definition (Führmann ’99)
A term t : A is said to be thunkable if it satisfies the equation
let x := t in λ(). x≡λ(). tThunkability intuitively captures “observational purity”
It does so generically, i.e. does not depend on effect considered
In a pure language, all terms are thunkable

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

32 / 54

Completely Unrelated Slide
Consider an effectful CBV λ-calculus.

Definition (Führmann ’99)
A term t : A is said to be thunkable if it satisfies the equation
let x := t in λ(). x≡λ(). tThunkability intuitively captures “observational purity”
It does so generically, i.e. does not depend on effect considered
In a pure language, all terms are thunkable

Theorem (Folklore Realizability)
The sublanguage of hereditarily thunkable terms satisfies full β-conversion.
f⊩A→B

:=

P.-M. Pédrot (INRIA, Gallinette team)∀u. u ⊩ A−→

f u thk

All your base categories are belong to us∧

fu⊩B
31/08/2020

32 / 54

Presheaves Are (Pure) Call-By-Value!

Now the magic trick.

TheoremA term t is thunkable in the Kripke semantics iff [t ]p is natural in p.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

33 / 54

Presheaves Are (Pure) Call-By-Value!

Now the magic trick.

TheoremA term t is thunkable in the Kripke semantics iff [t ]p is natural in p.

Psh(P) is the “pure” subcategory of an effectful CBV language!
This is a systematic construction that isn’t tied to Kripke semantics.
Unfortunately it relies on extensionality.
What about CBN?

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

33 / 54

Syntactic Models For FreeA CBN counterpart of thunkability is parametricity
Bernardy-Lasson ’11
There is a well-known parametricity interpretation for type theoryΓ `CIC M : A
where[[·]]ε := ·P.-M. Pédrot (INRIA, Gallinette team)−→[[Γ]]ε `CIC [M]ε : [[A]]ε M

and [[Γ, x : A]]ε := [[Γ]]ε , x : A, xε : [[A]]ε x

All your base categories are belong to us

31/08/2020

34 / 54

Syntactic Models For FreeA CBN counterpart of thunkability is parametricity
Bernardy-Lasson ’11
There is a well-known parametricity interpretation for type theoryΓ `CIC M : A
where[[·]]ε := ·−→[[Γ]]ε `CIC [M]ε : [[A]]ε M

and [[Γ, x : A]]ε := [[Γ]]ε , x : A, xε : [[A]]ε x

Turns out it is a syntactic model, compatible with intensionality!
It is a special case of a more general internal realizability interpretation.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

34 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

P.-M. Pédrot (INRIA, Gallinette team)x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

All your base categories are belong to us

31/08/2020

35 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

We have a bit of constraints. To get dependent elimination we need:1

Bε p x iff (x = λq α. tt) or (x = λq α. ff)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

35 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

We have a bit of constraints. To get dependent elimination we need:1

Bε p x iff (x = λq α. tt) or (x = λq α. ff)

2

in a unique way, i.e. b1 , b2 : Bε p x ` b1 = b2 (i.e. a HoTT proposition)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

35 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

We have a bit of constraints. To get dependent elimination we need:1

Bε p x iff (x = λq α. tt) or (x = λq α. ff)

2

in a unique way, i.e. b1 , b2 : Bε p x ` b1 = b2 (i.e. a HoTT proposition)

But we also critically need to be compatible with the presheaf structure!
3

That is, θBε (α : q ≤ p) : Bε p x → Bε q (α · x)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

35 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

We have a bit of constraints. To get dependent elimination we need:1

Bε p x iff (x = λq α. tt) or (x = λq α. ff)

2

in a unique way, i.e. b1 , b2 : Bε p x ` b1 = b2 (i.e. a HoTT proposition)

But we also critically need to be compatible with the presheaf structure!
3

That is, θBε (α : q ≤ p) : Bε p x → Bε q (α · x)

4

with further definitional functoriality to avoid coherence issues

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

35 / 54

On Parametric Presheaves
What does parametricity look like on the CBN presheaf model?
{
x:B

−→

x : (Π(q : P)(α : q ≤ p). B)xε : Bε p x

We have a bit of constraints. To get dependent elimination we need:1

Bε p x iff (x = λq α. tt) or (x = λq α. ff)

2

in a unique way, i.e. b1 , b2 : Bε p x ` b1 = b2 (i.e. a HoTT proposition)

But we also critically need to be compatible with the presheaf structure!
3

That is, θBε (α : q ≤ p) : Bε p x → Bε q (α · x)

4

with further definitional functoriality to avoid coherence issues

😱 Guess what? The CBV vs. CBN conundrum is back. 😱
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

35 / 54

Trouble All The Way Up
This is exactly the CBV vs. CBN conundrum one level higher
Either you pick Bε p x := (x = λq α. tt) + (x = λq α. ff)⇝ this satisfies unicity but breaks definitionality (i.e. CBV).

Or you freeify Bε p x := Πq α.(α · x = λr β. tt) + (α · x = λr β. ff)⇝ this satisfies definitionality but breaks unicity (i.e. CBN).

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

36 / 54

Trouble All The Way Up
This is exactly the CBV vs. CBN conundrum one level higher
Either you pick Bε p x := (x = λq α. tt) + (x = λq α. ff)⇝ this satisfies unicity but breaks definitionality (i.e. CBV).

Or you freeify Bε p x := Πq α.(α · x = λr β. tt) + (α · x = λr β. ff)⇝ this satisfies definitionality but breaks unicity (i.e. CBN).

It is not possible to get both at the same time in CIC!
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

36 / 54

Playing Cubes
We could solve this with infinite towers of parametricity.
That is, the n-level proof is guaranteed to be pure by then (n + 1)-level one.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

37 / 54

Playing Cubes
We could solve this with infinite towers of parametricity.
That is, the n-level proof is guaranteed to be pure by then (n + 1)-level one.

``Oh noes, not cubical type theory again!''

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

37 / 54

Playing Cubes
We could solve this with infinite towers of parametricity.
That is, the n-level proof is guaranteed to be pure by then (n + 1)-level one.

``Oh noes, not cubical type theory again!''But CuTT itself is justified by presheaf models.
What would be the point to implement presheaves using presheaves?
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

37 / 54

2 2(On the virtues of Authoritarianism.)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

38 / 54

It is a Revolution
Essentially, we were blocked on this issue since then. When suddenly...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

39 / 54

It is a Revolution
Essentially, we were blocked on this issue since then. When suddenly...
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.
Definitional proof-irrelevance without K.
Proc. ACM Program. Lang., 3(POPL):3:1–3:28, 2019.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

39 / 54

It is a Revolution
Essentially, we were blocked on this issue since then. When suddenly...
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.
Definitional proof-irrelevance without K.
Proc. ACM Program. Lang., 3(POPL):3:1–3:28, 2019.

They introduce a new sort SProp of strict propositions.
M, N : A : SProp−→ ` M ≡ N

A well-behaved subset of Prop compatible with HoTT
It enjoys all good syntactic properties

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

39 / 54

It is a Revolution
Essentially, we were blocked on this issue since then. When suddenly...
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau.
Definitional proof-irrelevance without K.
Proc. ACM Program. Lang., 3(POPL):3:1–3:28, 2019.

They introduce a new sort SProp of strict propositions.
M, N : A : SProp−→ ` M ≡ N

A well-behaved subset of Prop compatible with HoTT
It enjoys all good syntactic properties⇝ SProp is closed under products.
` A : □,

x : A ` B : SProp−→` Π(x : A). B : SProp⇝ Only False is eliminable from SProp into Type.
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

39 / 54

A Strict Doctrine
Possible Extension
sCIC additionally allows the elimination of eq from SProp to Type
This gives rise to a strict equality, i.e. sCIC has definitional UIP.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

40 / 54

A Strict Doctrine
Possible Extension
sCIC additionally allows the elimination of eq from SProp to Type
This gives rise to a strict equality, i.e. sCIC has definitional UIP.
When the libertarian HoTT freely adds infinite towers of equalities...
... the authoritarian sCIC will instead guillotine all higher equalities.

Art. 1. All humans are born uniquely equal in rights.
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

40 / 54

Strict Parametricity
In the parametric presheaf translation
Strict equality is the authoritarian way to solve the coherence hell.
make the parametricity predicate free ⇝ definitional functoriality
require it to be a strict proposition ⇝ proof uniqueness{x : Π(q ≤ p). [[A]]q
x : A −→xε : Π(q ≤ p). [[A]]ε q (α · x)
where critically [[A]]ε p x : SProp.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

41 / 54

Strict Parametricity
In the parametric presheaf translation
Strict equality is the authoritarian way to solve the coherence hell.
make the parametricity predicate free ⇝ definitional functoriality
require it to be a strict proposition ⇝ proof uniqueness{x : Π(q ≤ p). [[A]]q
x : A −→xε : Π(q ≤ p). [[A]]ε q (α · x)
where critically [[A]]ε p x : SProp.

We call the result the prefascist translation. (lat. fascis : sheaf)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

41 / 54

Strict Parametricity
In the parametric presheaf translation
Strict equality is the authoritarian way to solve the coherence hell.
make the parametricity predicate free ⇝ definitional functoriality
require it to be a strict proposition ⇝ proof uniqueness{x : Π(q ≤ p). [[A]]q
x : A −→xε : Π(q ≤ p). [[A]]ε q (α · x)
where critically [[A]]ε p x : SProp.

We call the result the prefascist translation. (lat. fascis : sheaf)

Theorem
The prefascist translation is a syntactic model of CIC into sCIC.
Full conversion, full dependent elimination.
The actual construction is a tad involved, but boils down to the above.
Unsurprinsingly, UIP is required to interpret universes (tricky!).
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

41 / 54

No Pain, No GainsCIC is way weaker than ETTsCIC is conjectured to enjoy the usual good syntactic properties.
Canonicity seems relatively easy to show
UIP makes reduction depend on conversion though
SN is problematic, e.g. sCIC + an impredicative universe is not SN
Hoping that SN holds in the predicative case, decidability follows

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

42 / 54

No Pain, No GainsCIC is way weaker than ETTsCIC is conjectured to enjoy the usual good syntactic properties.
Canonicity seems relatively easy to show
UIP makes reduction depend on conversion though
SN is problematic, e.g. sCIC + an impredicative universe is not SN
Hoping that SN holds in the predicative case, decidability follows
We don’t rely on impredicativity in the prefascist model
We would inherit the purported good properties sCIC for free.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

42 / 54

Back to Set
Set is a model of sCIC
Thus, the prefascist model can also be described set-theoretically.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

43 / 54

Back to Set
Set is a model of sCIC
Thus, the prefascist model can also be described set-theoretically.
A prefascist set A := (Ap , (−) ⊩p A) over a category P is given by
a family of sets Ap for p ∈ P.
a family of predicates (−) ⊩p A

P.-M. Pédrot (INRIA, Gallinette team)⊆

Conep (A) := Π(q : P)(α : q ≤ p). Aq

All your base categories are belong to us

31/08/2020

43 / 54

Back to Set
Set is a model of sCIC
Thus, the prefascist model can also be described set-theoretically.
A prefascist set A := (Ap , (−) ⊩p A) over a category P is given by
a family of sets Ap for p ∈ P.
a family of predicates (−) ⊩p A⊆

Conep (A) := Π(q : P)(α : q ≤ p). Aq

A prefascist morphism f from A to B isa family of functions fp : Elp A → Bp
preserving predicates, i.e.
∀x : Elp A.

appp (f, x) ⊩p B

where
Elp A

:= {x : Conep (A) | ∀q (α : q ≤ p). (α · x) ⊩q A}

appp (f, x) :=P.-M. Pédrot (INRIA, Gallinette team)λq (α : q ≤ p). fq (α · x)
All your base categories are belong to us

31/08/2020

43 / 54

Through The Looking Glass
Theorem
Prefascist sets over P form a category Pfs(P) with definitional laws.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

44 / 54

Through The Looking Glass
Theorem
Prefascist sets over P form a category Pfs(P) with definitional laws.

Theorem
As categories, Psh(P) and Pfs(P) are equivalent.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

44 / 54

Through The Looking Glass
Theorem
Prefascist sets over P form a category Pfs(P) with definitional laws.

Theorem
As categories, Psh(P) and Pfs(P) are equivalent.
Proving this requires extensionality principles!
Hence, in a set-theoretical meta, both describe the same objects
Yet, Pfs(P) is better behaved in an intensional settingThis could come in handy for higher category theory...

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

44 / 54

Through The Looking Glass
Theorem
Prefascist sets over P form a category Pfs(P) with definitional laws.

Theorem
As categories, Psh(P) and Pfs(P) are equivalent.
Proving this requires extensionality principles!
Hence, in a set-theoretical meta, both describe the same objects
Yet, Pfs(P) is better behaved in an intensional settingThis could come in handy for higher category theory...

Takeaway: prefascist sets are a better presentation of presheaves
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

44 / 54

ApplicationПО ВСЕМ
ОТРАСЛЯМ
ЛОГИКИ

Russian Constructivism
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

45 / 54

Russian Constructivist School
A splinter group of constructivists, whose core tenet can be summarized as:
Proofs are Kleene realizers

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

46 / 54

Russian Constructivist School
A splinter group of constructivists, whose core tenet can be summarized as:
Proofs are Kleene realizers
Thus, the principle that puts it apart both from Brouwer and Bishop:
Markov’s Principle (MP)∀(f : N → B). ¬¬(∃n : N. f n = tt) → ∃n : N. f n = tt
A lot of equivalent statements, e.g. a TM that doesn’t loop terminatesSemi-classical: HAω ⊊ HAω + MP ⊊ PAω
Known to preserve existence property (i.e. canonicity)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

46 / 54

Russian Constructivist School
A splinter group of constructivists, whose core tenet can be summarized as:
Proofs are Kleene realizers
Thus, the principle that puts it apart both from Brouwer and Bishop:
Markov’s Principle (MP)∀(f : N → B). ¬¬(∃n : N. f n = tt) → ∃n : N. f n = tt
A lot of equivalent statements, e.g. a TM that doesn’t loop terminatesSemi-classical: HAω ⊊ HAω + MP ⊊ PAω
Known to preserve existence property (i.e. canonicity)

What if we tried to extend CIC with MP through a syntactic model?
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

46 / 54

MP in Kleene Realizability
Let’s look at the realizer∀(f : N → B). ¬¬(∃n : N. f n = tt) → ∃n : N. f n = tt
let mp f _ :=let n := ref 0 in
while true do
if f !n then return n else n := n + 1
done

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

47 / 54

MP in Kleene Realizability
Let’s look at the realizer∀(f : N → B). ¬¬(∃n : N. f n = tt) → ∃n : N. f n = tt
let mp f _ :=let n := ref 0 in
while true do
if f !n then return n else n := n + 1
done

Proving mp ⊩ MP needs MP in the meta-theory!
As such, this is cheating
The realizer doesn’t use the doubly-negated proof
Relies on a semi-classical meta-theory and unbounded loops
We have little hope to implement this in CIC with a syntactic model

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

47 / 54

MP in Kleene Realizability
Let’s look at the realizer∀(f : N → B). ¬¬(∃n : N. f n = tt) → ∃n : N. f n = tt
let mp f _ :=let n := ref 0 in
while true do
if f !n then return n else n := n + 1
done

Proving mp ⊩ MP needs MP in the meta-theory!
As such, this is cheating
The realizer doesn’t use the doubly-negated proof
Relies on a semi-classical meta-theory and unbounded loops
We have little hope to implement this in CIC with a syntactic model

We need something else...
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

47 / 54

What Else?

Not one, but at least two alternatives!

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

48 / 54

What Else?

Not one, but at least two alternatives!

Coquand-Hofmann’s syntactic model for HAω + MP
Herbelin’s direct style proof using static exceptions

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

48 / 54

What Else?

Not one, but at least two alternatives!

Coquand-Hofmann’s syntactic model for HAω + MP
Herbelin’s direct style proof using static exceptions
CH’s model is a mix of Kripke semantics and Friedman’s A-translation
Kripke semantics ⇝ global cell p : N → B whereq≤p:=

q pointwise truer than p

A-translation ⇝ exceptions of type Ap := ∃n : N. p n = tt

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

48 / 54

What Else?

Not one, but at least two alternatives!

Coquand-Hofmann’s syntactic model for HAω + MP
Herbelin’s direct style proof using static exceptions
CH’s model is a mix of Kripke semantics and Friedman’s A-translation
Kripke semantics ⇝ global cell p : N → B whereq≤p:=

q pointwise truer than p

A-translation ⇝ exceptions of type Ap := ∃n : N. p n = tt
The secret sauce is that the exception type depends on the current p
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

48 / 54

Pipelining
Coquand-Hofmann’s model is a bit ad-hoc

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

49 / 54

Pipelining
Coquand-Hofmann’s model is a bit ad-hoc
Instead, we define the Calculus of Constructions with Completeness Principles as

CCCP(⊇ CIC)Exn−→

CIC + E

Pfs

−→

sCIC

Pfs is the prefascist model described before
Exn is the exceptional model, a CIC-worthy A-translation

Theorem
If sCIC enjoys The Good Properties™ then so does CCCP.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

49 / 54

Pipelining
Coquand-Hofmann’s model is a bit ad-hoc
Instead, we define the Calculus of Constructions with Completeness Principles as

CCCP(⊇ CIC)

Exn

−→

Pfs

CIC + E−→sCIC

Pfs is the prefascist model described before
Exn is the exceptional model, a CIC-worthy A-translation

Theorem
If sCIC enjoys The Good Properties™ then so does CCCP.
Exn is a very simple syntactic model of CIC
Pick a fixed type E of exceptions in the target theory.
`S A : □In particular−→[[¬A]]E

P.-M. Pédrot (INRIA, Gallinette team)`T [[A]]E : □ +∼=`T [A ]∅
E : E → [[A]]E[[A]]E → E

All your base categories are belong to us

31/08/2020

49 / 54

Monic FailWe perform the exceptional translation over an exotic type of exceptions
CCCP

Exn

−→

CIC + EIn the the prefascist model over N → B,

P.-M. Pédrot (INRIA, Gallinette team)

Pfs

−→

sCIC

Ep := Σn : N. p n = tt

All your base categories are belong to us

31/08/2020

50 / 54

Monic FailWe perform the exceptional translation over an exotic type of exceptions
CCCP

Exn

−→

CIC + EIn the the prefascist model over N → B,

Pfs

−→

sCIC

Ep := Σn : N. p n = tt

We also have a modality in CIC + E
local[local φ A ]p

: (N → B) → □ → □:= [A ]p∧φ∼return : A → local φ A
local commutes to arrows and positive types
local φ E ∼= E + (Σn : N. φ n = tt)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

50 / 54

Monic FailWe perform the exceptional translation over an exotic type of exceptions
CCCP

Exn

−→

CIC + EIn the the prefascist model over N → B,

Pfs

−→

sCIC

Ep := Σn : N. p n = tt

We also have a modality in CIC + E
local[local φ A ]p

: (N → B) → □ → □:= [A ]p∧φ∼return : A → local φ A
local commutes to arrows and positive types
local φ E ∼= E + (Σn : N. φ n = tt)

Theorem
CCCP validates MP.
Proof by symbol pushing in CIC + E by the above and [[¬A]]E ∼= [[A]]E → E.
P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

50 / 54

A Computational Analysis of MP
Every time we go under local we get new exceptions!
local φ E∼=

E + (Σn : N. φ n = tt)

return is a delimited continuation prompt / static exception binder.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

51 / 54

A Computational Analysis of MP
Every time we go under local we get new exceptions!
local φ E∼=

E + (Σn : N. φ n = tt)

return is a delimited continuation prompt / static exception binder.
The structure of the realizer thus follows closely Herbelin’s proof.
mp (p : ¬¬(∃n. f n = tt)) :=tryα ⊥e (p (λk. k (λn. raiseα n))) with α n 7→ n

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

51 / 54

A Computational Analysis of MP
Every time we go under local we get new exceptions!
local φ E∼=

E + (Σn : N. φ n = tt)

return is a delimited continuation prompt / static exception binder.
The structure of the realizer thus follows closely Herbelin’s proof.
mp (p : ¬¬(∃n. f n = tt)) :=tryα ⊥e (p (λk. k (λn. raiseα n))) with α n 7→ nThus, Herbelin’s proof is the direct style variant of Coquand-Hofmann

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

51 / 54

Final Digression
This is also highly reminiscent of NbE models
Two canonical ways to extend Kripke completeness to positive types:
Add neutral terms to the semantic of positive types
Add MP in the meta

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

52 / 54

Final Digression
This is also highly reminiscent of NbE models
Two canonical ways to extend Kripke completeness to positive types:
Add neutral terms to the semantic of positive types
Add MP in the meta
Neutral terms behave as statically bound exceptions
As our model shows, this two techniques are morally equivalent.
This also highlights suspicious ties between delimited continuations andpresheaves.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

52 / 54

Conclusion
On presheaves:
Presheaves are the pure fragment of an effectful CBV language
We gave a computationally better-behaved presentation of presheaves
It is a syntactic model that relies on strict equality in the target
Provides for free extensions of CIC with SN, canonicity and the like... assuming sCIC enjoys this (†)

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

53 / 54

Conclusion
On presheaves:
Presheaves are the pure fragment of an effectful CBV language
We gave a computationally better-behaved presentation of presheaves
It is a syntactic model that relies on strict equality in the target
Provides for free extensions of CIC with SN, canonicity and the like... assuming sCIC enjoys this (†)
On MP:
Static exceptions as a composition prefascist + exceptions
This provides a computational extension of CIC that validates MP

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

53 / 54

Conclusion
On presheaves:
Presheaves are the pure fragment of an effectful CBV language
We gave a computationally better-behaved presentation of presheaves
It is a syntactic model that relies on strict equality in the target
Provides for free extensions of CIC with SN, canonicity and the like... assuming sCIC enjoys this (†)
On MP:
Static exceptions as a composition prefascist + exceptions
This provides a computational extension of CIC that validates MP
TODO:
Implement cubical type theory in this model

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

53 / 54

Scribitur ad narrandum, non ad probandum

Thanks for your attention.

P.-M. Pédrot (INRIA, Gallinette team)All your base categories are belong to us

31/08/2020

54 / 54