search

VictorCMiraldo / reg-diff

Diffing experiment for a simpler universe
0 stars 0 forks source link

Make Spine into a bi-functor #8

Open VictorCMiraldo opened 7 years ago

VictorCMiraldo commented 7 years ago

I really do not like the nasty β trick on the Scns constructor:

data S (P : ΠΠSet) : U → Set where
    Scp  : {ty : U} → S P ty
    Schg : {ty : U}(i j : Constr ty)
         → P (typeOf ty i) (typeOf ty j)
         → S P ty
    Scns : {ty : U}(i : Constr ty)
         → All (contr P ∘ β) (typeOf ty i)
         → S P ty

Maybe, making S into a bifunctor will make things simpler. Something in the lines of:

data S (P : ΠΠSet)(Q : AASet)(ty : U) : Set where
    Scp  : S P ty
    Schg : (i j : Constr ty)
         → P (typeOf ty i) (typeOf ty j)
         → S P ty
    Scns : (i : Constr ty)
         → All (contr Q) (typeOf ty i)
         → S P ty
pedagand commented 7 years ago

Alleluia! I was thinking of the same thing just now..

VictorCMiraldo commented 7 years ago

We should be solving this and issue 9 together.

https://github.com/VictorCMiraldo/reg-diff/issues/9