effectfully/1-effectfully.md Secret

## 1-effectfully.md

      
    Raw
  

              1-effectfully.md
            
          
вместе с правилами enc dec = id и dec enc = id.

enc . dev = id and dec . enc = id, I suppose?

Pi_Beta      (A:U)(B:A->U)(f: Pi A B)    : Path (Pi A B) (\(x:A) -> f x) f

Why is the eta rule for (->) called Pi_Beta?

протащили в путь: Path (B a) -> Path (Pi A B).

This is a type error.

потом попробуем закодировать самый базовый Пи-тип на котором строится вся теория MLTT, и докажем вторую часть задания.
<...>
 PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B)
   = (app A B,lam A B,Pi_Beta A B,Pi_Eta A B)

 Pi (A: U) (B: A -> U)
   : U = (x:A) -> B(x)
 lam (A: U) (B: A -> U) (b: Pi A B)
   : Pi A B = \(x: A) -> b x
 app (A: U) (B: A -> U) (f: Pi A B) (a: A)
   : B a = f a
 Pi_Beta (A: U) (B: A -> U) (f: Pi A B)
   : Path (Pi A B) (\(x:A) -> f x) f
 Pi_Eta (A: U) (B: A -> U) (f: Pi A B)
   : Path (Pi A B) f (\(x:A) -> f x)


You "encode" Pi by aliasing the built-in (->) (not even fully, because the type of B still contains (->)) and then proceed with proving that Pi A B is isomorphic to Pi A B which it of course is, because it's just the same type, which is fine, because we can have non-trivial isomorphism between A and A (like the isomorphism induced by not : Bool -> Bool), but your isomorphism is the trivial one (i.e. the one induced by id : A -> A):

 lam (A: U) (B: A -> U) (b: Pi A B)
   : Pi A B = \(x: A) -> b x
 app (A: U) (B: A -> U) (f: Pi A B) (a: A)
   : B a = f a


This doesn't show us anything apart from the fact that binding a variable in a telescope is the same thing as binding a variable via lambda which is not a very interesting property. This example doesn't even show that you have the eta-conversion rule, because both lam and app bind f and a and apply f to a (only lam calls f b). You could at least make it

 lam (A: U) (B: A -> U) (b: Pi A B)
   : Pi A B = b
 app (A: U) (B: A -> U) (f: Pi A B) (a: A)
   : B a = f a


There is also a question of why lam is called the way it is.
This part:

во-вторых, покажем, что в кодировке Пи у нас функция равна своей аппликации (да да, вам не послышалось).
Теперь докажем вторую задачу и главный номер представления (то, что функция равна своей аппликации, ну бредятина же на звук!):

is just a really ambiguous wording. It sounds like you would prove either f = f x (which is nonsense) or f = app f (which is fine), but you do neither of these things and instead prove something trivial about the way you handle telescopes.

  
## 2-5HT.md

      
    Raw
  

              2-5HT.md
            
          
    Hello, @effectfully!
I made clear the part where we need to hack classic beta rule to show that we are working in the category of endofunctors. Path (B a) is a partial application so it can be type checked perfectly. Specifying the composition without symbol . is ok for me, see nothing wrong with it. Nonsense is only in a way how you interpret the article.
Of course, we need to be careful when we do term rewriting, as even when we don't change the semantics of the term we could easily change the syntax of the term (e.g. from telescope to body), so maybe we can't name this lambda calculus no more as we hacked one rule. But in the category of Pi endofunctors lam should be equal to app anyway, we just make it clear and visible in beta rule adjustment.
Once you claimed I was unable to encode Sigma through Pi and stated seriously that this was impossible. Now you are claiming I have some errors, but for me seems everything legit and perfectly embeds not only into isomorphism as it should theoretically, but also it shows PTS embedding pretty straightforward and simple.

  
## 3-effectfully.md

      
    Raw
  

              3-effectfully.md
            
          
Specifying the composition without symbol . is ok for me, see nothing wrong with it.

How do you distinguish it from function application then? g . f is a standard syntax (as well as f ; g), why confuse people by using a really ambiguous notation?

Path (B a) is a partial application so it can be type checked perfectly.

Yes, but not Path (B a) -> ..., because in A -> ... A has to be of type Type and Path (B a) is not of this type. Unless you overload (->) too.

Nonsense is only in a way how you interpret the article.

I do not interpret the article as nonsense and I only used this word where you used it as well:

то, что функция равна своей аппликации, ну бредятина же на звук!


Once you claimed I was unable to encode Sigma through Pi and stated seriously that this was impossible.

I still state you can't do that in a vanilla MLTT. I also rejected all your attempts to encode Sigma in terms of Pi in Agda. If you have any more of them, I'm happy to provide evidence they're not correct as well or apologize for being ignorant.

Now you are claiming I have some errors, but for me seems everything legit and perfectly embeds not only into isomorphism as it should theoretically, but also it shows PTS embedding pretty straightforward and simple.

I'm claiming that

you have a minor error with Path (B a) -> Path (Pi A B)
you have an ambiguous notation for function composition
the Pi_Beta (A: U) (B: A -> U) (f: Pi A B) : Path (Pi A B) (\(x:A) -> f x) f and Pi_Eta (A: U) (B: A -> U) (f: Pi A B) : Path (Pi A B) f (\(x:A) -> f x) rules are the same eta rule for functions (provided Path is symmetric which I suppose it is). I do not understand why you use the Beta word there
that entire example with Pi is no more interesting than a proof that id1 (A: U) (x: A) : A = x is equal to id2 (A: U) : A -> A = \(x: A) -> x, because the only difference between lam and app is in whether you bind the x argument using the telescopic syntax or a lambda. I.e. this example is not theoretically interesting at all


But in the category of Pi endofunctors lam should be equal to app anyway

What are the denotations of lam and app? To me, they look literally the same modulo this telescopic syntax. Their denotations could be different if the target theory has telescopes as well, but I presume that your category does not care about telescopes and they get denotated away. So... what's the difference between lam and app then?

  
## 4-5HT.md

      
    Raw
  

              4-5HT.md
            
          
    This is very funny:

you have a minor error with Path (B a) -> Path (Pi A B)
you have an ambiguous notation for function composition

Seems you're completely ignoring my comments.

I still state you can't do that in a vanilla MLTT.

Even if we have it encoded in PTS, cubicaltt? Well, that way of rejecting peer reviewed proofs is extraordinary for me. Why you don't just ignore what I'm doing? Do you understand that you're in couple messages from the forever ban?

So... what's the difference between lam and app then?

The way I put it no difference. That's the point of the article.

  
## 5-effectfully.md

      
    Raw
  

              5-effectfully.md
            
          
you have a minor error with Path (B a) -> Path (Pi A B)
you have an ambiguous notation for function composition

Just to clarify, I'm not saying this flaws are any more serious than just typos.

Seems you're completely ignoring my comments.

I'm not. Maybe I just misunderstood something.

Why you don't just ignore what I'm doing?

Someone gave me a link, I couldn't resist to leave a comment.

Even if we have it encoded in PTS, cubicaltt? Well, that way of rejecting peer reviewed proofs is extraordinary for me.

Well, obviously cubicalltt is not a vanilla MLTT. Also the paper does have Sigma built-in. So what is your reference?
Here is my reference:

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.
-- Thorsten Dr Thorsten Altenkirch, somewhere on the Agda mailing list


Do you understand that you're in couple messages from the forever ban?

That's fine.

  
## 6-5HT.md

      
    Raw
  

              6-5HT.md
            
          
    Some false facts from your statements to beat your arrogance:

Obviously cubicalltt is not a vanilla MLTT. Also the paper does have Sigma built-in. So what is your reference?

MLTT does include Sigma type starting from 1972 paper. That doesn't mean we can't settle a task to express Sigma by using only PI. Stop using word obviously when you're trying to bully or troll people. You should be more exact and ruthless.

I also rejected all your attempts to encode Sigma in terms of Pi in Agda.

I had zero attempts to do this in Agda, but any of my students can do that. Here is pts and cubicaltt: https://tonpa.guru/stream/2017/2017-10-28%20Pure%20Sigma.htm

That's fine.

Submission line. It seems your target is not to find the truth or make an adjustment for understanding but to make controversy from nothing. Ban.

  
## 7-effectfully.md

      
    Raw
  

              7-effectfully.md
            
          
MLTT does include Sigma type starting from 1972 paper.

I did not say an MLTT does not have Sigma, I said you can't encode it. Sigma' = Sigma is not an encoding, just an alias.

I had zero attempts to do this in Agda

I've just checked, you're correct, that wasn't Agda, but a couple of other dependently typed languages. Here was you first attempt:

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


My response:

you also need fst and snd
Your Σ is a recursor rather than eliminator (albeit slightly dependent) and to define snd you need some form of induction

You answered:

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.

And then

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.

Then we had a long chat and finally you proposed to build the term myself

I just put you an idea of encoding Sigma we have not finished all this stuff
Your claim that this is not possible will be declined
...
mean it should be something like that
I don't know yet, @zraffer should
there should be some Congruence passed as param, that I know for sure
I'm pretty sure you're capable of building this term.

The logs

but any of my students can do that.

I'd be happy to receive any evidence from anybody that Sigma can be encoded in terms of Pi.

Stop using word obviously when you're trying to bully or troll people. You should be more exact and ruthless.

But cubicalltt is by no means a form of vanilla MLTT. Or do you disagree with that?

Submission line. It seems your target is not to find the truth or make an adjustment for understanding but to make controversy from nothing.

Nah, it's just the case that if you ban me, I can stop arguing with you, which is a nice consequence for both of us.

  
## 8-5HT.md

      
    Raw
  

              8-5HT.md
            
          
    I do not want to ban physically, I assume you're an adult person and will stop writing to me. But if it is necessary I can ban physically. Are you OK with that, dude?

  
## 9-effecfully.md

      
    Raw
  

              9-effecfully.md
            
          
    THIS MESSAGE WAS LOST.
I ask here whether 5HT is going to cut my cables which I would appreciate and say that I'm trying to have a healthy discussion.

  
## 91-5HT.md

      
    Raw
  

              91-5HT.md
            
          
    Do you know that Github has ban functionality?

  
## 92-effectfully.md

      
    Raw
  

              92-effectfully.md
            
          
https://tonpa.guru/stream/2017/2017-10-28%20Pure%20Sigma.htm

Nice attempt, but this is not Sigma. There you have
data Sigma (A: Type) (P: A -> Type) (x:A): Type
   = (intro: (y:P x) -> Sigma A P)

(minor typo: I suppose it should be Sigma A P x?), but it's simply not Sigma A P, your encoding contains that x which you might think is a minor thing, but it's not.

  
## 93-5HT.md

      
    Raw
  

              93-5HT.md
            
          
    Which healthy things you would bring next? Isn't writing an article as an answer to your bullshit a constructive and healthy enough? Can you prove that there is no transport function from one Sigma definition to another?

  
## 94-effectfully.md

      
    Raw
  

              94-effectfully.md
            
          
Isn't writing an article as an answer a constructive and healthy enough?

That's very healthy indeed.

bullshit

That's not.

Can you prove that there is no transport function from one Sigma definition to another?

There are transports, but not the isomorphism, because types do not match:
data TrueSigma (A : Set) (P : A -> Set) : Set where
  trueSigma : (x : A) -> P x -> TrueSigma A P

trueFst : ∀ {A P} -> TrueSigma A P -> A
trueFst (trueSigma x _) = x

data FalseSigma (A : Set) (P : A -> Set) x : Set where
  falseSigma : P x -> FalseSigma A P x

trueToFalse : ∀ {A P} -> (p : TrueSigma A P) -> FalseSigma A P (trueFst p)
trueToFalse (trueSigma x y) = falseSigma y

falseToTrue : ∀ {A P x} -> FalseSigma A P x -> TrueSigma A P
falseToTrue (falseSigma y) = trueSigma _ y

open import Relation.Binary.PropositionalEquality

iso₁ : ∀ {A P} -> (p : TrueSigma A P) -> falseToTrue (trueToFalse p) ≡ p
iso₁ (trueSigma _ _) = refl

-- Type error.
iso₂ : ∀ {A P x} -> (p : FalseSigma A P x) -> trueToFalse (falseToTrue p) ≡ p
iso₂ p = {!!}
Of course, there can't be an isomorphism, because TrueSigma A P is bigger than FalseSigma A P x, i.e. in general, TrueSigma A P has more inhabitants than FalseSigma A P x, because in the former case x is not fixed and can be any.
Your sigma is not existential, it doesn't allow you to forget type information. Can you define a list of tuples each containing a natural number representing length and vector of that length with your Sigma? Where "list" is the usual one and natural numbers are distinct:
data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

  
## 95-5HT.md

      
    Raw
  

              95-5HT.md
            
          
    @effectfully, I have made my choice. You are not welcome here.