Dependent types over Church-encoded type in PTS/CoC I'm experimenting with pure type systems in Barendregt's lambda cube, specifically with the most powerfull one, the Calculus of Constructions. This system has sorts * and BOX. Just for the record, below I'm using the concrete syntax of the Morte tool https://github.com/Gabriel439/Haskell-Morte-Library which is close to the classical lambda calculus.

I see we can emulate inductive types by some kind of Church-like encoding (a.k.a. Boehm-Berarducci isomorphism for algebraic data types).
For a simple example I use type Bool = ∀(t : *) -&gt; t -&gt; t -&gt; t with the constructors True = λ(t : *) -&gt; λ(x : t) -&gt; λ(y : t) -&gt; x and False = λ(t : *) -&gt; λ(x : t) -&gt; λ(y : t) -&gt; y.

I see that the type of term-level functions Bool -&gt; T is isomorphic to pairs of type Product T T with classical Product = λ(A : *) -&gt; λ(B : *) -&gt; ∀(t : *) -&gt; (A -&gt; B -&gt; t) -&gt; t modulo parametricity by means of function if : Bool -&gt; λ(t : *) -&gt; t -&gt; t -&gt; t which is in fact identity. 

All questions below will be about representations of dependent types Bool -&gt; *.


I can split D : Bool -&gt; * into pair of D True and D False. Are there the canonical way to create D again? I want to reproduce isomosphism Bool -&gt; T = Product T T by an analogue of function if at type level but I cannot write this function as simple as original if because we cannot pass kinds in arguments like types.
I use a kind of an inductive type with two constuctors to solve question(1). The high level description (Agda-style) is the following type (used instead of type-level if)

data BoolDep (T : *) (F : *) : Bool -&gt; * where
  DepTrue : T -&gt; BoolDep T F True
  DepFalse : F -&gt; BoolDep T F False


with the following encoding in PTS/CoC:

λ(T : *) -&gt; λ(F : *) -&gt; λ(bool : Bool ) -&gt;
∀(P : Bool -&gt; *) -&gt;
∀(DepTrue : T -&gt; P True ) -&gt;
∀(DepFalse : F -&gt; P False ) -&gt;
P bool


Is my encoding above correct?
I can write down the constructors for BoolDep like this code for DepTrue : ∀(T : *) -&gt; ∀(F : *) -&gt; T -&gt; BoolDep T F True:

λ(T : *) -&gt;  λ(F : *) -&gt;  λ(arg : T ) -&gt;
λ(P : Bool -&gt; *) -&gt;
λ(DepTrue : T -&gt; P True ) -&gt;
λ(DepFalse : F -&gt; P False ) -&gt;
DepTrue arg



but I cannot write down the inverse function (or any function in the inverse direction). Is it possible? Or should I use another representation for BoolDep to produce an isomorphism BoolDep T F True = T?
You can't do this using the traditional Church encoding for Bool:

#Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool


... because you can't write a (useful) function of type:

#Bool → *


The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types.

There are at least three ways you can solve this:


Use the Calculus of Inductive Constructions.  Then you could generalize the type of #Bool to:

#Bool = ∀(n : Nat) → ∀(Bool : *ₙ) → ∀(True : Bool) → ∀(False : Bool) → Bool


... and then you would instantiate n to 1, which means you could pass in *₀ as the second argument, which would type-check because:

*₀ : *₁


... so then you could use #Bool to select between two types.
Add one more sort:

* : □ : △


Then you would define a separate #Bool₂ type like this:

#Bool₂ = ∀(Bool : □) → ∀(True : Bool) → ∀(False : Bool) → Bool


This is essentially a special case of the Calculus of Inductive constructions, but produces less reusable code since now we must maintain two separate definitions of #Bool, one for each sort that we wish to support.
Encode #Bool₂ directly within the Calculus of Constructions as:

#Bool₂ = ∀(True : *) → ∀(False : *) → *



If the goal is to use this directly within unmodified morte then only approach #3 will work.