Hello @mietek! I'm very glad that you come to our channel. Give me a chance to describe our needs and strategy.

In simple our project could be described as CiC translations to CoC.

Idea is to have simple core in prover.

Classical CoC consists of two universes, but we extended it with infinite.

Our CoC type checker supports both predicative and impredicative non-comulative hierarchies.

What we already know:

- CoC 2 universes (Terms/Types or Star/Box) — is known to be consistent
- CoC + Infinite Predicative Hierarchy — is known to be consistent
- CoC + 1 Impredicative Low Level + Inifinite Predicative — is known to be consistent

What we don't know is a consistency of

- CoC + Infinite Impredicative Hierarchy that is enabled by default in OM typechecker (Our Intermediate Language).

Why We did that strange configuration?

Because we took Morte Base Library that is build for Impredicative Hierarchieds. Predicative mode of OM can't typecheck it and we have no time to rewrite all libarary, despite it is demo library in Church-like encoding (which is ineffective and display bad performance).

So we will use classical configuration of Prop + Infinite Predicative Hierarchies in EXE (Top Level Language) and we can compile (translates, macro-expand) it to Impredicative Infinite OM Hierarchies.

What you can suggest us?

We have demo encoding of Bool Induction compiled to Impredicative Infinite CoC PTS here:

https://github.com/groupoid/om/blob/master/priv/posets/Data/Bool/induc

https://github.com/groupoid/om/blob/master/priv/posets/Data/Bool/induc

There is also a deny paper but in was written for another PTS configiration:

http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz

http://www.cs.ru.nl/~herman/PUBS/IndNonder.ps.gz

EXE is planned as a Idris-like practical language with ability to model HIT homotopy types.

- Full OM Typechecker: https://github.com/groupoid/om/blob/master/src/om_type.erl
- Predicativity/Impredicativity trigger: https://github.com/groupoid/om/blob/master/src/om.erl#L142-L143
- Some terms in EXE Language: https://github.com/groupoid/exe/tree/master/priv/Exe/logic

Hope you will find our project useful and interesting.

We also known as company who made top-10 github Erlang project web framework N2O.

Our full open source portfolio is at http://5ht.co

Our strategy is to bring native theorem prover for Erlang platform.

And rewrite our libraries to EXE.

As for now we have no money to pay you, but if you can provide some expertise I will try to find some compensation for you. Also you can consider to join us if this projects would be useful for you.

All our projects are completely driven by ourselves (3 people) and are under MIT-like licenses.

Hi @5HT! I’ve noticed your work a while ago; I think it was because you had a repo of the Charity language.

I think there is a problem with infinite impredicativity, but I’m not an expert.

yes I grab it from Canadians and put everything on Github + papers :-)

For sure there is. If two impredicative universes leads to inconsistency, then infinite should.

New Place of Charity: https://github.com/devaspot/charity

Yeah.

I found a *second* implementation.

I don’t remember where, though.

Charity was my step to undestanding all the stuff

So — you don’t know if CoC + infinite impredicative hierarchy is consistent, but you suspect it is not?

for us would be nice to see simple and clean Agda code to see CoC + predicative or impredicative Model.

You can start with CoC + predicative infinity.

It is for sure consistent.

But simplicity of the model is a key point.

I found couple of models in Agda but not satisfied with them.

As for the question itself, I would also suspect CoC+I.I.H. is not consistent, but I don’t know how to show that. hm. Would that involve showing Girard’s paradox, I wonder?

we have no time to rewrite all library

Why is that?

I haven’t looked closely at Morte, but I would be surprised if rewriting its library took a long time. It can’t be very large, can it?

It was ASCII compatible with Morte One but now it is not

I can’t really read this, but I’ve been living in Agda for a year, and I’m pretty sure I could rewrite Agda’s standard library, cutting away half of the code

Production Library will be translated from EXE to OM.

So I would think that having a library should not be the reason for building on top of a questionable base

we will rewrite some DepTypes prelude (I'm looking forward to Coq's one) to EXE

I gave you a link to sample EXE terms.

It doesn't matter Agda, Coq, having DepType language it is easy to port any terms

OK. Perhaps I still don’t understand the reason why you want to have an infinite impredicative hierarchy.

You are right, but seems that @zraffer have technique to compile EXE PIH to COC IIH

all the type-check would be done in PIH, and the translated with macros to IIH core

as it seems for him that IIH is more efficient one in terms of size.

so everything could be changed.

But it also could be that IIH is consistent, as it has infinity and not limited.

I thought it was interesting that you’re building stuff in Erlang.

anyway it would be nice to have OM model in Agda.

not to shaking hands in space :-)

To me, Erlang’s actor-based approach is still the way I think about real-world problems.

We are only thinking about real apps and applicate EXE to real world problems.

As you know in Ukraine our friends did LING, custom Erlang VM implementations.

All code in EXE would be DepTyped. So yes, we will have Session Types.

Actually we already using typed protocols in Erlang.

I don't know yet full model as I will write in EXE as it comes available.

OK. I’m asking because it still seems to be an active research topic.

We have current SPEC for BERT terms and Typed Erlang Records that are checked in compile time.

I’m interested in this, but I’m following it at a certain distance; I’m doing other things.

We will have Comonad for replacing gen_server

and strict protocol description with EXE records (aka contexts).

I don't see what to research here, to be honest.

Effect system is also could be stolen from Idris, or other implementations.

```
(record effect (v:Type) (r:Type): Type :=
(values: v)
(resource: r)
(computation: (v → r))
(handler: effect v r → monad effect v r))
(data monad_eff (eff: list effect) (m: Type → Type) (a: Type): Type :=
(intro: eff m a xs (\ (v: Type) → xs) → monad_eff xs m a))
(record handler (e: effect) (m: Type → Type): Type :=
(action: ∀ (r: res) (eff: e t res resk) (k: ∀ (x: t) → resk x → m a) → m a))
```

I don’t think this is a very good solution

But that’s what people are doing

My main problem with that is that it assumes you are in control of both endpoints

Mundo paper.

Effects in Idris seem fine, although I don’t have that much experience with them. I like row polymorphism for records in PureScript; I think it also reuses it for effects.

So — thinking like an Erlang programmer — session types must be able to deal with the situation where you only control one endpoint and the other one is untrusted.

I haven’t seen research into session types which would consider the problem of the other party deviating from the protocol.

I don’t understand why; this seems like a crucially important thing.

as for session type system we will have a chance to investigate having working compiler.

That is the nearest milestone for us.

The approach I would consider would be, treat protocols as state machines; automata

With every message, progress the state of the automaton

And… somehow… types

;)

I think this might be the closest

This might’ve been the first paper on the subject

Sadly Honda died unexpectedly

to receive grands, etc.

mostly political reasons.

OK, so you want your theorem prover to be capable of supporting the work that is currently being in fashion.

Makes sense.

to be complete modern technology stack.

Consider Lisp, with quote, eval, and the ability to intensionally analyse quoted terms.

Right?

Metacircularity is building an infinite tower of languages, then handwaving to collapse the tower.

Right?

This postulates QITs, and is also rather complex.

I’m not thinking about dependent types for now.

I’m thinking about simple types.

Still, I don’t want to do metacircularity, or type-theory-in-type-theory.

Have you looked at it?

There are some examples in https://github.com/mietek/et-language/blob/master/doc/pdf/splawski-1993.pdf

In IPL (unlike SML) equality between terms of arbitrary types is decidable.

We reject papers with built-in Recorsors, Inductions W types, etc.

Yes. I know about encodings, and I think that’s the wrong approach for what I’m trying to do.

Interesting. Why?

We also don't need Equality in Prover Core.

only definitional in type checker.

this is our working categorical model.

Fibrational Dialgebras, LCCC.

Right. I thought this was related because they seem to do everything by encoding, and Hermann was cataloguing encodings before they wrote this.

WIP

The reason WHY we reject Equ Fixpoint W-Def RecurP InducP in core of the provers.

Because it all are HACKS to Type Theory for easy bootstrap.

It has all built-in already.

We just want to extract it from space.

I don’t understand enough about the more advanced type theories; I’m working with non-dependent theories in a dependently-typed language.

Yes. So, in simply-typed lambda calculus, we can Church-encode naturals as folds, right?

But we can’t give an induction principle for the naturals.

As far as I understand, the smallest extension of STLC in which we can, is Gödel’s system T.

T includes the induction principle as a primitive — this is what you describe as a hack, yes?

We have primitives for everything else — lambda abstraction, products, etc

Why not primitives for datatypes?

because System T was made by human, and CoC + IH is not made by anyone. It comes from LCCC.

To me, it is the encodings which seem like hacks.

All comes from that, this is the core of computational theory.

Encoding are natural way of construct inductive data types.

If was discovered by Church but not finished in Inductive Theory.

It was fixed when Coquand built Coq.

The smallest extension of STLC which supports encoding induction principles is system F, right?

Universal quantification on types.

But that’s a pretty big extension.

You see, the problem is that Vertices of Lambda Cube besides top (Pw) and bottom (Untyped Lamnda) are very limited.

We propose to work only in top and extract (by erasure of type info) to bottom tgeory.

This could be done purely without introducing anything besides ONE type.

Pi type — is ONE Type we need. It expands to 4 type judgment rules and can compute the Entire Multiverse.

STCL, Sytem F, System T, System Fw — are lacks this feature.

:-)

or similar stuff

but not in pure CoC

having Inductive Encoding.

```
(record sigma (A: Type) (B: A → Type): Type :=
(pr1: A)
(pr2: B pr1))
```

Sigma in EXE.

records are themselves sigmas

Just as You can encode List Cons Constructor.

Cons — is a record.

actually codata

aka Stream

How do you do records in pure CoC?

@mietek, may I ask why are you interested in simple types? They seem so weak.

CoC includes any type inside. You just need to express it in MLTT language.

@effectfully, I’m interested in understanding things in very small increments.

@mietek you will not find the truth in STLC, System F, T, Fw.

:-)

I’m interested in justification logic, or explicit provability logic (not Gödel-Löb provability).

But this is perhaps off-topic for this channel.

Actually any Code in OM can be translated directly to any language (includes Agda).

Because it contains only Pi and Lambdas.

If you’d like to talk about that, I invite you to join #dependent on Freenode/IRC.

can you encode proper sigma?

Artemov was a professor in Moscow. http://web.archive.org/web/20050308034922/http://www.cs.gc.cuny.edu/~sartemov/

Is anyone here perhaps familiar with his work?

Or that of his students? http://home.inf.unibe.ch/~kuznets/JLBibliography.html

He was a PhD student of Kolmogorov.

@effectfully you are not a first who came without proofs and says that something is not possible :-)

Also feel free to ask questions. I spent a year banging my head against this.

despite being a russian

we already declined one article.

well, if it's possible to get sigma via pi, it should be simple

Some of the lectures and exercises are in English, as well. They helped me.

didn't even know there are lectures about intuitionistic logic in russian

@5HT, thanks for the explanation. I think your project is quite interesting, and I will keep an eye on it. I don’t think I’ll have the time to collaborate, though, as it’s sufficiently more advanced than what I’m doing at the moment.

I’ll need to catch up first!

@effectfully, well, it is Brouwer, Heyting, and *Kolmogorov*, right?

I think there is a strong Russian constructivist tradition.

@effectfully, I don’t want to spam here… come to #dependent if you’re interested.

And anyone else, too.

You can talk

OK, thanks for all the pointers, I need to do some studies first, before I have something to say or ask

Thorsten Altenkirch:

Ok, when we think of homogenous tuples AxA then this can also be

understood as a function 2 -> A. This also works for heterogenous tuples

like AxB using dependent functions Pi x:2.if x then A else B. However the

next logical step is Sigma x:A.B x, which have no good representations as

functions (unless we accept very dependent functions which in my mind goes

against the spirit of type theory). For this reason it seems to me that

the generalisation from -> to Pi and from x to Sigma is the primary one,

and the fact that tuples can be represented as functions is secondary.

"which have no good representations" and you concluded "I claim that NO representation" :-)

nice reading )

@5HT, he didn't give a proof (which is not the same as don't have a proof), so it's his word against yours. Altenkirch wins.

and you said it can be done in Agda

```
definition Sigma := λ (A: Type),
λ (B: A -> Type),
∀ (DepProd: Type),
∀ (Make: (∀ (_1: A), ∀ (_2: B _1), DepProd) ),
DepProd
print Sigma
print result:
definition EXE.Sigma : Π (A : Type), (A → Type) → Type :=
λ (A : Type) (B : A → Type), Π (DepProd : Type), (Π (_1 : A), B _1 → DepProd) → DepProd
```

Lean Prover.

```
$ cat Sigma/@
λ (A: *)
→ λ (B: A -> *)
→ ∀ (Prod2: *)
→ ∀ (Make:
∀ (_1: A)
→ ∀ (_2: B _1)
→ Prod2)
→ Prod2
$ om sh
> om:type(om:a("#Sigma/@")).
{{"∀",{'A',0}},
{{star,1},
{{"∀",{'B',0}},
{{{"∀",{'_',0}},{{var,{'A',0}},{star,1}}},{star,1}}}}}
```

OM Prover.

here I posted only formation axiom

Having proper formation formulated, anything else is just a technique.

could you show it in Agda? Your

`Σ`

is a recursor rather than eliminator (albeit slightly dependent) and to define `snd`

you need some form of induction
Lean would be good too, though I would prefer Agda

I gave you proper Lean code. If you can't encode simple Church type, and you can't translate it to Agda, I have nothing to say you more, sorry.

As I said I have different activities here.

Please, educate yourself.

here is what I have

```
{-# OPTIONS --type-in-type #-}
Σ : (A : Set) -> (A -> Set) -> Set
Σ A B = (P : Set) -> (∀ x -> B x -> P) -> P
fst : ∀ {A B} -> Σ A B -> A
fst p = p _ (λ x _ -> x)
snd : ∀ {A B} -> (p : Σ A B) -> B (fst p)
snd p = p _ (λ x y -> {!!})
```

when you have time and desire of course

why do you need Type-In-Type?

It is not needed to encode Sigma in Church encoding.

This is snd

```
λ (A: *)
→ λ (B: A -> *)
→ λ (_1: A)
→ λ (_2: B _1)
→ λ (product: #Sigma/@ A B) → _2
```

```
definition snd := λ (A: Type),
λ (B: A -> Type),
λ (_1: A),
λ (_2: B _1),
λ (P: Sigma A B),
_2
print snd
print result:
definition EXE.snd : Π (A : Type) (B : A → Type) (_1 : A), B _1 → Sigma A B → B _1 :=
λ (A : Type) (B : A → Type) (_1 : A) (_2 : B _1) (P : Sigma A B), _2
```

Lean Prover.

```
> rp(om:erase(om:a("#Sigma/snd"))).
{{{"λ",{'_1',0}},
{any,{{"λ",{'_2',0}},
{any,{{"λ",{product,0}},{any,{var,{'_2',0}}}}}}}},
{{"∀",{'A',0}},
{{star,1},
{{"∀",{'B',0}},
{{{"∀",{'_',0}},{{var,{'A',0}},{star,1}}},
{{"∀",{'_1',0}},
{{var,{'A',0}},
{{"∀",{'_2',0}},
{{app,{{var,{'B',0}},{var,{'_1',0}}}},
{{"∀",{product,0}},
{{{"∀",{'Prod2',0}},
{{star,1},
{{"∀",{'Make',0}},
{{{"∀",{'_1',0}},
{{var,{'A',0}},
{{"∀",{'_2',0}},
{{app,{{var,{'B',0}},{var,{'_1',0}}}},{var,{'Prod2',0}}}}}},
{var,{'Prod2',0}}}}}},
{app,{{var,{'B',0}},{var,{'_1',0}}}}}}}}}}}}}}}
ok
```

Compiled Erlang Code:

```
> 'Sigma':
'Make'/0 fst/0 module_info/0 module_info/1 snd/0
```

Hope you'll find it useful.

I can also encode Metatheoretical Π:

```
record Π (A: Type): Type :=
(Π: (A → Type) → Type)
(fun: (B: A → Type) → ∀ (a: A) → B a → Π B)
(app: (B: A → Type) → Π B → ∀ (a: A) → B a)
(app-fun (B: A → Type) (f: ∀ (a: A) → B a): ∀ (a: A) → app (fun f) a = (fun-app (B: A → Type) (p: Π B): fun (λ(a: A) → app p a) ==> p)
```

what you can include in your PhD articles :-)

Recursor and Induction are not available in Church encoding by design for DepTypes.

we already told you that.

That is why we're creating Lambek Encoding.

but eliminators for Sigma are the same as for Prod.

As I already mentioned.