These are chat archives for groupoid/exe

19th
Aug 2016
Namdak Tonpa
@5HT
Aug 19 2016 12:01
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:
  1. CoC 2 universes (Terms/Types or Star/Box) — is known to be consistent
  2. CoC + Infinite Predicative Hierarchy — is known to be consistent
  3. CoC + 1 Impredicative Low Level + Inifinite Predicative — is known to be consistent
What we don't know is a consistency of
  1. CoC + Infinite Impredicative Hierarchy that is enabled by default in OM typechecker (Our Intermediate Language).
Why We did that strange configuration?
Namdak Tonpa
@5HT
Aug 19 2016 12:07
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
There is also a deny paper but in was written for another PTS configiration:
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.
Namdak Tonpa
@5HT
Aug 19 2016 12:13
Links:
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.
Namdak Tonpa
@5HT
Aug 19 2016 12:22
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.
Miëtek Bak
@mietek
Aug 19 2016 13:11
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.
Namdak Tonpa
@5HT
Aug 19 2016 13:12
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
Miëtek Bak
@mietek
Aug 19 2016 13:13
I was wondering where you found that.
Namdak Tonpa
@5HT
Aug 19 2016 13:14
On their institute public servers
Miëtek Bak
@mietek
Aug 19 2016 13:14
Actually, no, sorry — I’m confused.
Yeah.
I found a second implementation.
I don’t remember where, though.
Namdak Tonpa
@5HT
Aug 19 2016 13:15
Cool
Charity was my step to undestanding all the stuff
Miëtek Bak
@mietek
Aug 19 2016 13:16
So — you don’t know if CoC + infinite impredicative hierarchy is consistent, but you suspect it is not?
Namdak Tonpa
@5HT
Aug 19 2016 13:16
Yes
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.
Miëtek Bak
@mietek
Aug 19 2016 13:19
I can definitely relate to that.
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?
Namdak Tonpa
@5HT
Aug 19 2016 13:21
I mean our Morte/Om base library: https://github.com/groupoid/om/tree/master/priv/normal
It was ASCII compatible with Morte One but now it is not
Miëtek Bak
@mietek
Aug 19 2016 13:23
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
Namdak Tonpa
@5HT
Aug 19 2016 13:23
It is a toy library for OM demoes.
Production Library will be translated from EXE to OM.
Miëtek Bak
@mietek
Aug 19 2016 13:23
In fact, a number of people have their own Agda libraries
So I would think that having a library should not be the reason for building on top of a questionable base
Namdak Tonpa
@5HT
Aug 19 2016 13:23
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
So I would think that having a library should not be the reason for building on top of a questionable base
Miëtek Bak
@mietek
Aug 19 2016 13:25
OK. Perhaps I still don’t understand the reason why you want to have an infinite impredicative hierarchy.
Namdak Tonpa
@5HT
Aug 19 2016 13:25
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.
Miëtek Bak
@mietek
Aug 19 2016 13:28
OK. I’m not really qualified to comment.
Namdak Tonpa
@5HT
Aug 19 2016 13:28
but I said OM support both PIH and IIH
so everything could be changed.
But it also could be that IIH is consistent, as it has infinity and not limited.
Miëtek Bak
@mietek
Aug 19 2016 13:29
I thought it was interesting that you’re building stuff in Erlang.
Namdak Tonpa
@5HT
Aug 19 2016 13:29
I'm not SURE yet.
anyway it would be nice to have OM model in Agda.
not to shaking hands in space :-)
Miëtek Bak
@mietek
Aug 19 2016 13:30
To me, Erlang’s actor-based approach is still the way I think about real-world problems.
Namdak Tonpa
@5HT
Aug 19 2016 13:30
We are only thinking about real apps and applicate EXE to real world problems.
Miëtek Bak
@mietek
Aug 19 2016 13:30
This message was deleted
Namdak Tonpa
@5HT
Aug 19 2016 13:31
That's why we took Erlang Virtual machines.
Miëtek Bak
@mietek
Aug 19 2016 13:31
Does your system allow typed message-passing?
Namdak Tonpa
@5HT
Aug 19 2016 13:32
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.
Miëtek Bak
@mietek
Aug 19 2016 13:33
Session types: are you building on any specific formalisation?
Namdak Tonpa
@5HT
Aug 19 2016 13:34
And we have Haskell demo implementation http://5ht.co/n2o.htm
I don't know yet full model as I will write in EXE as it comes available.
Miëtek Bak
@mietek
Aug 19 2016 13:34
OK. I’m asking because it still seems to be an active research topic.
Namdak Tonpa
@5HT
Aug 19 2016 13:34
We have current SPEC for BERT terms and Typed Erlang Records that are checked in compile time.
Miëtek Bak
@mietek
Aug 19 2016 13:35
I’m interested in this, but I’m following it at a certain distance; I’m doing other things.
Namdak Tonpa
@5HT
Aug 19 2016 13:35
For me it is simple.
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
Namdak Tonpa
@5HT
Aug 19 2016 13:43
you mean Idris-like effect system or Mundo paper?
Miëtek Bak
@mietek
Aug 19 2016 13:43
My main problem with that is that it assumes you are in control of both endpoints
Mundo paper.
Namdak Tonpa
@5HT
Aug 19 2016 13:43
Personally me deny all papers with C-like code ;-)
Miëtek Bak
@mietek
Aug 19 2016 13:44
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.
Namdak Tonpa
@5HT
Aug 19 2016 13:44
Then np, we agreed on Effect system :-)
Miëtek Bak
@mietek
Aug 19 2016 13:46
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.
Namdak Tonpa
@5HT
Aug 19 2016 13:46
as for session type system we will have a chance to investigate having working compiler.
That is the nearest milestone for us.
Miëtek Bak
@mietek
Aug 19 2016 13:48
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
;)
Namdak Tonpa
@5HT
Aug 19 2016 13:49
protocols are interfaces, the automata is comonad with it laws.
I think this might be the closest
Namdak Tonpa
@5HT
Aug 19 2016 13:50
When I see japanese in the paper I internally trust it :-)
This might’ve been the first paper on the subject
Sadly Honda died unexpectedly
Namdak Tonpa
@5HT
Aug 19 2016 13:52
Cool stuff thanks!
Miëtek Bak
@mietek
Aug 19 2016 13:56
Why are you interested in HIT/HoTT?
Namdak Tonpa
@5HT
Aug 19 2016 13:56
to be sure we have complete technology.
Miëtek Bak
@mietek
Aug 19 2016 13:57
Can you expand?
Namdak Tonpa
@5HT
Aug 19 2016 13:57
so universities can join in.
to receive grands, etc.
mostly political reasons.
Miëtek Bak
@mietek
Aug 19 2016 13:58
OK, so you want your theorem prover to be capable of supporting the work that is currently being in fashion.
Makes sense.
Namdak Tonpa
@5HT
Aug 19 2016 13:58
yes.
to be complete modern technology stack.
Miëtek Bak
@mietek
Aug 19 2016 13:59
I’m interested in doing reflection properly.
Namdak Tonpa
@5HT
Aug 19 2016 13:59
reflection?
Miëtek Bak
@mietek
Aug 19 2016 14:00
Consider Lisp, with quote, eval, and the ability to intensionally analyse quoted terms.
Right?
Namdak Tonpa
@5HT
Aug 19 2016 14:00
metacircularity?
Miëtek Bak
@mietek
Aug 19 2016 14:00
No.
Metacircularity is building an infinite tower of languages, then handwaving to collapse the tower.
Right?
Namdak Tonpa
@5HT
Aug 19 2016 14:01
metacircularity is not possible in Dependent Theory as I know.
Miëtek Bak
@mietek
Aug 19 2016 14:01
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.
Namdak Tonpa
@5HT
Aug 19 2016 14:02
Seems it needs to work in Altenkirch's Cubical Type Theory
Miëtek Bak
@mietek
Aug 19 2016 14:03
I’ve seen you’ve starred https://github.com/mietek/et-language
Have you looked at it?
Namdak Tonpa
@5HT
Aug 19 2016 14:04
not yet, haven't found iplman.pdf
Miëtek Bak
@mietek
Aug 19 2016 14:05
Yes, unfortunately Spławski’s PhD is not public…
Namdak Tonpa
@5HT
Aug 19 2016 14:06
we rather working in contemporary mindset of Encodings
Miëtek Bak
@mietek
Aug 19 2016 14:06
But, there are two important things visible in the examples:
In IPL (unlike SML) equality between terms of arbitrary types is decidable.
Namdak Tonpa
@5HT
Aug 19 2016 14:06
Church-Boem-Berrarducci, Scott, Parigot, CPS ...
We reject papers with built-in Recorsors, Inductions W types, etc.
Miëtek Bak
@mietek
Aug 19 2016 14:07
Yes. I know about encodings, and I think that’s the wrong approach for what I’m trying to do.
Interesting. Why?
Namdak Tonpa
@5HT
Aug 19 2016 14:07
We will have Equality written in pure CoC.
We also don't need Equality in Prover Core.
only definitional in type checker.
Miëtek Bak
@mietek
Aug 19 2016 14:08
Namdak Tonpa
@5HT
Aug 19 2016 14:08
sure
this is our working categorical model.
Fibrational Dialgebras, LCCC.
Miëtek Bak
@mietek
Aug 19 2016 14:09
Right. I thought this was related because they seem to do everything by encoding, and Hermann was cataloguing encodings before they wrote this.
Namdak Tonpa
@5HT
Aug 19 2016 14:09
This is our Categorical Model of Encoding: https://github.com/groupoid/exe/tree/master/priv/Lean
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.
Miëtek Bak
@mietek
Aug 19 2016 14:12
Well, hold on. I’m with you part of the way.
Namdak Tonpa
@5HT
Aug 19 2016 14:12
CCC doesn't need it.
It has all built-in already.
We just want to extract it from space.
Miëtek Bak
@mietek
Aug 19 2016 14:13
I don’t understand enough about the more advanced type theories; I’m working with non-dependent theories in a dependently-typed language.
Namdak Tonpa
@5HT
Aug 19 2016 14:13
Andromedans are doing similar way.
Miëtek Bak
@mietek
Aug 19 2016 14:13
Consider the natural numbers.
Namdak Tonpa
@5HT
Aug 19 2016 14:13
OK. Simple Inductive Type.
Miëtek Bak
@mietek
Aug 19 2016 14:13
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.
Namdak Tonpa
@5HT
Aug 19 2016 14:14
In STLC can't in CoC we can.
Miëtek Bak
@mietek
Aug 19 2016 14:14
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?
Namdak Tonpa
@5HT
Aug 19 2016 14:15
yes
Miëtek Bak
@mietek
Aug 19 2016 14:15
I’m not sure why is that a hack.
We have primitives for everything else — lambda abstraction, products, etc
Why not primitives for datatypes?
Namdak Tonpa
@5HT
Aug 19 2016 14:16
because System T was made by human, and CoC + IH is not made by anyone. It comes from LCCC.
Miëtek Bak
@mietek
Aug 19 2016 14:16
I’ll need to learn more about LCCC, then.
To me, it is the encodings which seem like hacks.
Namdak Tonpa
@5HT
Aug 19 2016 14:16
CCC has only terminals, products and exponentials.
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.
Miëtek Bak
@mietek
Aug 19 2016 14:17
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.
Namdak Tonpa
@5HT
Aug 19 2016 14:18
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.
effectfully
@effectfully
Aug 19 2016 14:21
you can't emulate Sigma using just Pi
Namdak Tonpa
@5HT
Aug 19 2016 14:21
So we are not interested in them at all.
:-)
effectfully
@effectfully
Aug 19 2016 14:21
well, you can if you have insane/very dependent types
or similar stuff
but not in pure CoC
Namdak Tonpa
@5HT
Aug 19 2016 14:21
You can encode Sigma type in pure CoC.
having Inductive Encoding.
  (record sigma (A: Type) (B: A → Type): Type :=
         (pr1: A)
         (pr2: B pr1))
Sigma in EXE.
effectfully
@effectfully
Aug 19 2016 14:22
there are no records in pure CoC
records are themselves sigmas
Namdak Tonpa
@5HT
Aug 19 2016 14:22
We Can Compile Polynomial Functors in Pure CoC.
Just as You can encode List Cons Constructor.
Cons — is a record.
actually codata
aka Stream
Miëtek Bak
@mietek
Aug 19 2016 14:23
A bit confused.
How do you do records in pure CoC?
Namdak Tonpa
@5HT
Aug 19 2016 14:24
you can use simplest Berrarducci Encoding.
Miëtek Bak
@mietek
Aug 19 2016 14:25
You said codata… but does CoC have codata?
Miëtek Bak
@mietek
Aug 19 2016 14:25
Sorry, I have no idea how to read that.
effectfully
@effectfully
Aug 19 2016 14:25
@mietek, may I ask why are you interested in simple types? They seem so weak.
Namdak Tonpa
@5HT
Aug 19 2016 14:25
CoC includes any type inside. You just need to express it in MLTT language.
Miëtek Bak
@mietek
Aug 19 2016 14:25
@effectfully, I’m interested in understanding things in very small increments.
Namdak Tonpa
@5HT
Aug 19 2016 14:26
Please Read Explanations of Berrarducci Encoding.
@mietek you will not find the truth in STLC, System F, T, Fw.
Miëtek Bak
@mietek
Aug 19 2016 14:26
I’m interested in internalising alpha-equivalence.
effectfully
@effectfully
Aug 19 2016 14:26
you can't encode Sigma in terms of Pi — this is for sure
Namdak Tonpa
@5HT
Aug 19 2016 14:26
only full theory with infinity universes contains it.
:-)
effectfully
@effectfully
Aug 19 2016 14:27
@5HT, or maybe you can give an example in Agda?
Namdak Tonpa
@5HT
Aug 19 2016 14:27
You misunderstand something :-)
Miëtek Bak
@mietek
Aug 19 2016 14:27
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.
Namdak Tonpa
@5HT
Aug 19 2016 14:27
Actually any Code in OM can be translated directly to any language (includes Agda).
Because it contains only Pi and Lambdas.
effectfully
@effectfully
Aug 19 2016 14:28
@mietek, thanks for the answer
Miëtek Bak
@mietek
Aug 19 2016 14:28
If you’d like to talk about that, I invite you to join #dependent on Freenode/IRC.
Namdak Tonpa
@5HT
Aug 19 2016 14:28
I gave you an example of Product (this a a case of Sigma).
Miëtek Bak
@mietek
Aug 19 2016 14:29
Actually maybe one thing is not off-topic
Namdak Tonpa
@5HT
Aug 19 2016 14:29
in term of theory this is Cartesian part of CCC.
Miëtek Bak
@mietek
Aug 19 2016 14:29
I’m following the work of Sergei Artemov.
effectfully
@effectfully
Aug 19 2016 14:29
products are weaker than sigmas, of course
can you encode proper sigma?
Namdak Tonpa
@5HT
Aug 19 2016 14:30
not in Berrarducci, maybe, but yes this is possible.
effectfully
@effectfully
Aug 19 2016 14:31
I claim, this is not
Is anyone here perhaps familiar with his work?
He was a PhD student of Kolmogorov.
Namdak Tonpa
@5HT
Aug 19 2016 14:33
@effectfully you are not a first who came without proofs and says that something is not possible :-)
effectfully
@effectfully
Aug 19 2016 14:33
@mietek, could you suggest a paper to start with?
Miëtek Bak
@mietek
Aug 19 2016 14:33
Yes. :) This one.
effectfully
@effectfully
Aug 19 2016 14:34
thanks
Miëtek Bak
@mietek
Aug 19 2016 14:34
Also feel free to ask questions. I spent a year banging my head against this.
effectfully
@effectfully
Aug 19 2016 14:35
@5HT, I don't have a proof, but you neither
Namdak Tonpa
@5HT
Aug 19 2016 14:35
we are working
effectfully
@effectfully
Aug 19 2016 14:35
I find it very hard to understand what russians write
despite being a russian
Namdak Tonpa
@5HT
Aug 19 2016 14:35
just don't be so impatient
we already declined one article.
effectfully
@effectfully
Aug 19 2016 14:36
well, if it's possible to get sigma via pi, it should be simple
Namdak Tonpa
@5HT
Aug 19 2016 14:36
it is.
Miëtek Bak
@mietek
Aug 19 2016 14:36
Here’s something in Russian: http://lpcs.math.msu.su/~artemov/handouts/
Some of the lectures and exercises are in English, as well. They helped me.
Namdak Tonpa
@5HT
Aug 19 2016 14:37
Sorry guys, have no time to spend more here.
effectfully
@effectfully
Aug 19 2016 14:38
didn't even know there are lectures about intuitionistic logic in russian
Miëtek Bak
@mietek
Aug 19 2016 14:38
@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
@effectfully
Aug 19 2016 14:39
I mean, modern lecture notes
Miëtek Bak
@mietek
Aug 19 2016 14:40
Ah.
@effectfully, I don’t want to spam here… come to #dependent if you’re interested.
And anyone else, too.
Namdak Tonpa
@5HT
Aug 19 2016 14:42
It's ok
You can talk
effectfully
@effectfully
Aug 19 2016 14:43
OK, thanks for all the pointers, I need to do some studies first, before I have something to say or ask
effectfully
@effectfully
Aug 19 2016 14:53

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.

Namdak Tonpa
@5HT
Aug 19 2016 14:54
"which have no good representations" and you concluded "I claim that NO representation" :-)
nice reading )
effectfully
@effectfully
Aug 19 2016 14:54
@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.
Namdak Tonpa
@5HT
Aug 19 2016 14:54
ok ok I got it.
effectfully
@effectfully
Aug 19 2016 14:55
there is the "unless we accept very..." part
Namdak Tonpa
@5HT
Aug 19 2016 14:55
Unless we add anything that blow our mind to prover core :-)
effectfully
@effectfully
Aug 19 2016 14:55
yes, but you talk about CoC
and you said it can be done in Agda
Namdak Tonpa
@5HT
Aug 19 2016 15:10
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.
Namdak Tonpa
@5HT
Aug 19 2016 15:18
$ 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.
effectfully
@effectfully
Aug 19 2016 15:23
you also need fst and snd
Namdak Tonpa
@5HT
Aug 19 2016 15:23
they are just eliminators of Make introduction
here I posted only formation axiom
Having proper formation formulated, anything else is just a technique.
effectfully
@effectfully
Aug 19 2016 15:31
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
Namdak Tonpa
@5HT
Aug 19 2016 15:32
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.
effectfully
@effectfully
Aug 19 2016 15:33
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
Namdak Tonpa
@5HT
Aug 19 2016 20:13
just returned
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
Namdak Tonpa
@5HT
Aug 19 2016 20:33
OM Prover.
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
Namdak Tonpa
@5HT
Aug 19 2016 20:38
Compiled Erlang Code:
> 'Sigma':
'Make'/0       fst/0          module_info/0  module_info/1  snd/0
Hope you'll find it useful.
Namdak Tonpa
@5HT
Aug 19 2016 20:48
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 :-)
Namdak Tonpa
@5HT
Aug 19 2016 20:55
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.