An Attempt

It's time to return to AoPA and proceed with defining all the remaining relational operators, in hope of finally solving optimisation problems! It seems that when division comes into play, the problem about predicativity becomes even severer. Shin said "Since the only arrow having type ←₁ is ∈, we may be able to create specialised version of division to get around such problems?", but I don't quite understand what he means. (XD) Instead I wondered whether it is possible to make the sets ordinary values and thus eliminating the need for multiple versions of arrows, compositions, etc. As an inexperienced dependently-typed programmer, the only thing I can do is trying. So here it goes.

Relations are still defined in the same way.

_←_ : Set -> Set -> Set1
B ← A = A -> B -> Set

In order to make the type of sets a member of Set, I tried the following definition:

data §et (A : Set) (P : A -> Set) : Set where
  set : §et A P

The information (proposition) that characterises the set is put in the type. Some operations about sets can be easily implemented. Since all the relevant information is in the types, the sole purpose of the terms is carrying the types.

_∪_ : {A : Set} {P Q : A -> Set} ->
      §et A P -> §et A Q -> §et A (\a -> P a ⊎ Q a)
set ∪ set = set

_∩_ : {A : Set} {P Q : A -> Set} ->
      §et A P -> §et A Q -> §et A (\a -> P a × Q a)
set ∩ set = set

∈ : {A : Set} {P : A -> Set} -> A ← §et A P
∈ {P = P} set a = P a

Λ : {A B : Set} -> (R : B ← A) -> (a : A) -> §et B (R a)
Λ R a = set

Inclusion can now be defined as a relation between sets.

_⊆_ : {A : Set} {P Q : A -> Set} -> §et A Q ← §et A P
_⊆_ {P = P} {Q = Q} set set = forall a -> P a -> Q a

When I'm proving its reflexivity and transitivity, this definition makes Agda's pattern matching mechanism behave in a way I've never seen before. Fortunately it doesn't cause much problem.

⊆-refl : {A : Set} {P : A -> Set} {s : §et A P} -> s ⊆ s
⊆-refl {s = set} = \a Pa -> Pa

⊆-trans : {A : Set} {P₁ P₂ P₃ : A -> Set}
          {s₁ : §et A P₁} {s₂ : §et A P₂} {s₃ : §et A P₃} ->
          s₁ ⊆ s₂ -> s₂ ⊆ s₃ -> s₁ ⊆ s₃
⊆-trans {s₁ = set} {s₂ = set} {s₃ = set} s₁⊆s₂ s₂⊆s₃ =
  \a P₁a -> s₂⊆s₃ a (s₁⊆s₂ a P₁a)

So far so good. But difficulty emerged when I was trying to define relational fold. It's rather impossible to assign a type to the fold operator. Therefore I naturally stopped here.

I would guess this approach is very likely to fail. Even if foldR is successfully modelled, the entire AoPA has to be revised, which is a rather daunting task. XD

--
So it seems that we have to live with predicativity and all its consequences after all...?