[HoTT] 1D Mu Type

[Corlin Fardal <fardalcorlin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2547 bytes --]

I've managed to create a 1D Mu Type, essentially just a basis for creating 
any recursive higher inductive type with point and path constructors one 
could define. The construction is mainly based upon the paper "Higher 
Inductive Types in Programming," 
at http://www.cs.ru.nl/~herman/PUBS/HIT-programming.pdf. The construction 
reduces the path constructors to just one, by introducing a case term, and 
extends the polynomial functors to include function types, and introduces 
an application term and lambda term for the function types. To be able to 
deal with the new terms, the construction defines a type coercion function 
to make the path computation rule type check, but the way that it is 
defined makes it equal to the identity function, under case analysis that 
would compute down for any specific type. More details, of course, are in 
the Coq and Agda files attached to this post.

With this type we have a starting point for many next steps, including 
exploring the semantics of this new type, including showing that it gives 
rise to a cell monad, and showing homotopy initiality. Another next step 
would be seeing if we can define this type through some clever use of 
quotient types, perhaps in a similar way to the construction of 
propositional truncation.

I didn't write a paper about this, largely because it is just a fairly 
straight forward extension of an existing paper, and also because I'm not a 
terribly good writer, but I hope that this post suffices in sharing what 
little I've managed to accomplish. I also hope that this post doesn't seem 
too out of the ordinary for what's posted here, as this is the first thing 
I've ever posted, and I'm very new to this group in general, though I have 
read a good few things on here already, and from what I can tell, this 
doesn't seem too strange.

I checked various cases of HITs with my Mu type, and while the various 
constructors and induction rules seem to align with my intuition for what 
they should be, I don't actually know of anywhere where the induction rules 
for various kinds of inductive types exist, so I'd like to know if the 
definitions are correct, or if I messed anything up. In general, I'd be 
interested in anyone's thoughts about this.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2843 bytes --]

[-- Attachment #2: Mu1.agda --]
[-- Type: application/octet-stream, Size: 8234 bytes --]

{-# OPTIONS --without-K --rewriting #-}
open import Agda.Primitive

data _≡_ {a : Level} {A : Set a} (x : A) : A → Set a where
 refl : x ≡ x
{-# BUILTIN REWRITE _≡_ #-}
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data _+_ (A B : Set) : Set where
 inl : A → A + B
 inr : B → A + B

data _×_ (A B : Set) : Set where
 _,_ : A → B → A × B

data FCode : Set₁ where
 Id : FCode
 Const : Set → FCode
 Sum : FCode → FCode → FCode
 Prod : FCode → FCode → FCode
 Func : Set → FCode → FCode

FInter : FCode → Set → Set
FInter Id X = X
FInter (Const A) X = A
FInter (Sum F G) X = FInter F X + FInter G X
FInter (Prod F G) X = FInter F X × FInter G X
FInter (Func A F) X = A → FInter F X

FLift : {X : Set} (F : FCode) → (X → Set) → (FInter F X → Set)
FLift Id P x = P x
FLift (Const A) P _ = A
FLift (Sum F G) P (inl x) = FLift F P x
FLift (Sum F G) P (inr x) = FLift G P x
FLift (Prod F G) P (x , y) = FLift F P x × FLift G P y
FLift (Func A F) P f = (x : A) → FLift F P (f x)

all : {X : Set} (F : FCode) {P : X → Set} (f : (x : X) → P x) (x : FInter F X) → FLift F P x
all Id f x = f x
all (Const A) f a = a
all (Sum F G) f (inl x) = all F f x
all (Sum F G) f (inr x) = all G f x
all (Prod F G) f (x , y) = (all F f x , all G f y)
all (Func A F) f f' = λ x → all F f (f' x)

data TCode X F (c : FInter F X → X) : FCode → FCode → Set₁ where
 id : {G : FCode} → TCode X F c G G
 const : {G : FCode} {A : Set} → A → TCode X F c G (Const A)
 con : {G : FCode} → TCode X F c G F → TCode X F c G Id
 pi : {G H I : FCode} → TCode X F c G (Prod H I) → TCode X F c G H
 pi' : {G H I : FCode} → TCode X F c G (Prod H I) → TCode X F c G I
 pair : {G H I : FCode} → TCode X F c G H → TCode X F c G I → TCode X F c G (Prod H I)
 k : {G H I : FCode} → TCode X F c G H → TCode X F c G (Sum H I)
 k' : {G H I : FCode} → TCode X F c G I → TCode X F c G (Sum H I)
 case : {G H I J : FCode} → TCode X F c G (Sum H I) → TCode X F c (Prod G H) J → TCode X F c (Prod G I) J → TCode X F c G J
 app : {G H : FCode} {A : Set} → TCode X F c G (Func A H) → TCode X F c G (Const A) → TCode X F c G H
 lam : {G H : FCode} {A : Set} → TCode X F c (Prod G (Const A)) H → TCode X F c G (Func A H)

TInter : {X : Set} {F : FCode} (c : FInter F X → X) {G H :  FCode} → TCode X F c G H → FInter G X → FInter H X
TInter c id x = x
TInter c (const a) _ = a
TInter c (con t) x = c (TInter c t x)
TInter c (pi t) x with TInter c t x
...                          | (t' , _) = t'
TInter c (pi' t) x with TInter c t x
...                          | (_ , t') = t'
TInter c (pair t t') x = (TInter c t x , TInter c t' x)
TInter c (k t) x = inl (TInter c t x)
TInter c (k' t) x = inr (TInter c t x)
TInter c (case t f g) x with TInter c t x
...                                   | inl t' = TInter c f (x , t')
...                                   | inr t' = TInter c g (x , t')
TInter c (app f y) x = (TInter c f x) (TInter c y x)
TInter c (lam f) x = λ y → TInter c f (x , y)

TLift : {X : Set} {F : FCode} (c : FInter F X → X) {P : X → Set} (Pc : (x : FInter F X) → FLift F P x → P (c x)) {G H : FCode} (t : TCode X F c G H) (x : FInter G X) (Px : FLift G P x) → FLift H P (TInter c t x)
TLift c Pc id x Px = Px
TLift c Pc (const a) x Px = a
TLift c Pc (con t) x Px = Pc (TInter c t x) (TLift c Pc t x Px)
TLift c Pc (pi t) x Px with TInter c t x | TLift c Pc t x Px
...                                 | (t' , _)         | (Pt' , _) = Pt'
TLift c Pc (pi' t) x Px with TInter c t x | TLift c Pc t x Px
...                                  | (_ , t')         | (_ , Pt') = Pt'
TLift c Pc (pair t t') x Px = (TLift c Pc t x Px , TLift c Pc t' x Px)
TLift c Pc (k t) x Px = TLift c Pc t x Px
TLift c Pc (k' t) x Px = TLift c Pc t x Px
TLift c Pc (case t f g) x Px with TInter c t x | TLift c Pc t x Px
...                                           | inl t'           | Pt' = TLift c Pc f (x , t') (Px , Pt')
...                                           | inr t'          | Pt' = TLift c Pc g (x , t') (Px , Pt')
TLift c Pc (app f y) x Px = TLift c Pc f x Px (TInter c y x)
TLift c Pc (lam f) x Px = λ y → TLift c Pc f (x , y) (Px , y)

postulate Ext : (A : Set) (B : A → Set) (f g : (x : A) → B x) → ((x : A) → f x ≡ g x) → f ≡ g 
postulate Ext-inv-happly : (A : _) (B : _) (f : _) → Ext A B f f (λ _ → refl) ≡ refl
{-# REWRITE Ext-inv-happly #-}

coerce-eq : {X : Set} {F : FCode} (c : FInter F X → X) {P : X → Set} (f : (x : X) → P x) (Pc : (x : FInter F X) → FLift F P x → P (c x)) (fc : (x : FInter F X) → f (c x) ≡ Pc x (all F f x)) {G H : FCode} (t : TCode X F c G H) (x : FInter G X) → TLift c Pc t x (all G f x) ≡ all H f (TInter c t x)
coerce-eq c f Pc fc id x = refl
coerce-eq c f Pc fc (const a) x = refl
coerce-eq c f Pc fc (con t) x rewrite fc (TInter c t x) | coerce-eq c f Pc fc t x = refl
coerce-eq c f Pc fc (pi t) x rewrite coerce-eq c f Pc fc t x with TInter c t x
...                                                                                          | (t' , _) = refl
coerce-eq c f Pc fc (pi' t) x rewrite coerce-eq c f Pc fc t x with TInter c t x
...                                                                                           | (_ , t') = refl
coerce-eq c f Pc fc (pair t t') x rewrite coerce-eq c f Pc fc t x | coerce-eq c f Pc fc t' x = refl
coerce-eq c f Pc fc (k t) x rewrite coerce-eq c f Pc fc t x = refl
coerce-eq c f Pc fc (k' t) x rewrite coerce-eq c f Pc fc t x = refl
coerce-eq c f Pc fc (case t f' g) x rewrite coerce-eq c f Pc fc t x with TInter c t x
...                                                                                                     | inl t' rewrite coerce-eq c f Pc fc f' (x , t') = refl
...                                                                                                     | inr t' rewrite coerce-eq c f Pc fc g (x , t') = refl
coerce-eq c f Pc fc (app f' y) x rewrite coerce-eq c f Pc fc f' x = refl
coerce-eq c f Pc fc (lam f') x = Ext _ _ _ _ (λ y → coerce-eq c f Pc fc f' (x , y))

transp : {X : Set} (P : X → Set) {x y : X} → x ≡ y → P x → P y
transp P refl Px = Px

_,_=[_]=_ : {X : Set} (P : X → Set) {x y : X} → P x → x ≡ y → P y → Set
P , Px =[ p ]= Py = transp P p Px ≡ Py

ap : {X : Set} {P : X → Set} (f : (x : X) → P x) {x y : X} (p : x ≡ y) → P , f x =[ p ]= f y
ap f refl = refl

coerce : {X : Set} {F : FCode} (c : FInter F X → X) {P : X → Set} (f : (x : X) → P x) (Pc : (x : FInter F X) → FLift F P x → P (c x)) (fc : (x : FInter F X) → f (c x) ≡ Pc x (all F f x)) {G : FCode} (r t : TCode X F c G Id) (e : (x : FInter G X) → TInter c r x ≡ TInter c t x) (x : FInter G X) → P , TLift c Pc r x (all G f x) =[ e x ]= TLift c Pc t x (all G f x) → P , f (TInter c r x) =[ e x ]= f (TInter c t x)
coerce c f Pc fc r t e x h rewrite coerce-eq c f Pc fc r x | coerce-eq c f Pc fc t x = h

postulate Mu1 : (F G : FCode) (r t : (X : Set) (c : FInter F X → X) → TCode X F c G Id) → Set
postulate c : (F G : _) (r t : _) → FInter F (Mu1 F G r t) → Mu1 F G r t
postulate e : (F G : _) (r t : _) (x : FInter G (Mu1 F G r t)) → TInter (c F G r t) (r _ _) x ≡ TInter (c F G r t) (t _ _) x

postulate Mu1-ind : (F G : _) (r t : _) (P : Mu1 F G r t → Set) (Pc : (x : FInter F (Mu1 F G r t)) → FLift F P x → P (c _ _ _ _ x)) (Pe : (x : FInter G (Mu1 F G r t)) (Px : FLift G P x) → P , TLift (c _ _ _ _) Pc (r _ _) x Px  =[ e _ _ _ _ x ]= TLift (c _ _ _ _) Pc (t _ _) x Px) (x : Mu1 F G r t) → P x
postulate Mu1-ind-c : (F G : _) (r t : _) (P : _) (Pc : _) (Pe : _) (x : _) → Mu1-ind F G r t P Pc Pe (c _ _ _ _ x) ≡ Pc x (all F (Mu1-ind F G r t P Pc Pe) x)
{-# REWRITE Mu1-ind-c #-}
postulate Mu1-ind-e : (F G : _) (r t : _) (P : _) (Pc : _) (Pe : _) (x : _) → ap (Mu1-ind F G r t P Pc Pe) (e _ _ _ _ x) ≡ coerce (c _ _ _ _) (Mu1-ind F G r t P Pc Pe) Pc (λ x → refl) (r _ _) (t  _ _) (e _ _ _ _) x (Pe x (all G (Mu1-ind F G r t P Pc Pe) x))
{-# REWRITE Mu1-ind-e #-}

[-- Attachment #3: Mu1.v --]
[-- Type: application/octet-stream, Size: 5635 bytes --]

Open Scope type.

Inductive FCode :=
|Id : FCode
|Const : Type -> FCode
|Sum : FCode -> FCode -> FCode
|Prod : FCode -> FCode -> FCode
|Func : Type -> FCode -> FCode.

Definition FInter (F : FCode) (X : Type) : Type.
 induction F.
 exact X.
 exact T.
 exact (IHF1 + IHF2).
 exact (IHF1 * IHF2).
 exact (T -> IHF).
Defined.

Definition FLift {X} (F : FCode) (P : X -> Type) (x : FInter F X) : Type.
 induction F.
 exact (P x).
 exact T.
 destruct x.
 exact (IHF1 f).
 exact (IHF2 f).
 destruct x.
 exact (IHF1 f * IHF2 f0).
 exact (forall y, IHF (x y)).
Defined.

Definition all {X} (F : FCode) {P} (f : forall x : X, P x) x : FLift F P x.
 induction F.
 apply f.
 exact x.
 destruct x.
 apply IHF1.
 apply IHF2.
 destruct x.
 split.
 apply IHF1.
 apply IHF2.
 intro y.
 apply IHF.
Defined.

Inductive TCode {X F} (c : FInter F X -> X) : FCode -> FCode -> Type :=
|id : forall {G}, TCode c G G
|const : forall {G A}, A -> TCode c G (Const A)
|con : forall {G}, TCode c G F -> TCode c G Id
|pi : forall {G H I}, TCode c G (Prod H I) -> TCode c G H
|pi' : forall {G H I}, TCode c G (Prod H I) -> TCode c G I
|pair : forall {G H I}, TCode c G H -> TCode c G I -> TCode c G (Prod H I)
|k : forall {G H I}, TCode c G H -> TCode c G (Sum H I)
|k' : forall {G H I}, TCode c G I -> TCode c G (Sum H I)
|case : forall {G H I J}, TCode c G (Sum H I) -> TCode c (Prod G H) J -> TCode c (Prod G I) J -> TCode c G J
|app : forall {G H A}, TCode c G (Func A H) -> TCode c G (Const A) -> TCode c G H
|lam : forall {G H A}, TCode c (Prod G (Const A)) H -> TCode c G (Func A H).

Definition TInter {X F} (c : FInter F X -> X) {G H} (r : TCode c G H) (x : FInter G X) : FInter H X.
 induction r.
 exact x.
 exact a.
 apply c.
 apply IHr.
 exact x.
 destruct (IHr x).
 exact f.
 destruct (IHr x).
 exact f0.
 split.
 apply IHr1.
 exact x.
 apply IHr2.
 exact x.
 left.
 apply IHr.
 exact x.
 right.
 apply IHr.
 exact x.
 destruct (IHr1 x).
 apply IHr2.
 split.
 exact x.
 exact f.
 apply IHr3.
 split.
 exact x.
 exact f.
 apply (IHr1 x).
 exact (IHr2 x).
 intro y.
 apply IHr.
 split.
 exact x.
 exact y.
Defined.

Definition TLift {X F} (c : FInter F X -> X) {P} (Pc : forall x, FLift F P x -> P (c x)) {G H} (r : TCode c G H) x (Px : FLift G P x) : FLift H P (TInter c r x).
 induction r.
 exact Px.
 exact a.
 apply Pc.
 apply IHr.
 exact Px.
 assert (FLift (Prod H I) P (TInter c r x)).
 apply IHr.
 exact Px.
 simpl.
 destruct (TInter c r x).
 destruct X0.
 exact f1.
 assert (FLift (Prod H I) P (TInter c r x)).
 apply IHr.
 apply Px.
 simpl.
 destruct (TInter c r x).
 destruct X0.
 exact f2.
 split.
 apply IHr1.
 exact Px.
 apply IHr2.
 exact Px.
 apply IHr.
 exact Px.
 apply IHr.
 exact Px.
 assert (FLift (Sum H I) P (TInter c r1 x)).
 apply IHr1.
 exact Px.
 simpl.
 destruct (TInter c r1 x).
 apply IHr2.
 split.
 exact Px.
 exact X0.
 apply IHr3.
 split.
 exact Px.
 exact X0.
 apply IHr1.
 exact Px.
 intro y.
 apply IHr.
 split.
 exact Px.
 exact y.
Defined.

Axiom Ext : forall A B (f g : forall x : A, B x), (forall x, f x = g x) -> f = g.

Definition coerce_eq {X F} (c : FInter F X -> X) {P} (f : forall x : X, P x) (Pc : forall x, FLift F P x -> P (c x)) (fc : forall x, f (c x) = Pc x (all F f x)) {G H} (r : TCode c G H) x : TLift c Pc r x (all G f x) = all H f (TInter c r x).
 induction r.
 reflexivity.
 reflexivity.
 simpl.
 rewrite fc.
 rewrite IHr.
 reflexivity.
 simpl.
 rewrite IHr.
 simpl.
 destruct (TInter c r x).
 reflexivity.
 simpl.
 rewrite IHr.
 simpl.
 destruct (TInter c r x).
 reflexivity.
 simpl.
 rewrite IHr1.
 rewrite IHr2.
 reflexivity.
 simpl.
 rewrite IHr.
 reflexivity.
 simpl.
 rewrite IHr.
 reflexivity.
 simpl.
 rewrite IHr1.
 simpl.
 destruct (TInter c r1 x).
 simpl.
 rewrite IHr2.
 reflexivity.
 simpl.
 rewrite IHr3.
 reflexivity.
 simpl.
 rewrite IHr1.
 reflexivity.
 simpl.
 apply Ext;intros.
 rewrite IHr.
 reflexivity.
Defined.

Axiom Ext_inv_happly : forall A B f, Ext A B f f (fun _ => eq_refl) = eq_refl.

Definition transp {X P} {x y : X} (p : x = y) (Px : P x) : P y :=
match p with
|eq_refl => Px
end.

Definition depeq {X P} {x y : X} (p : x = y) (px : P x) (py : P y) := transp p px = py.

Notation "px =[ p ]= py" := (depeq p px py) (at level 50).

Definition ap {X P} (f : forall x : X, P x) {x y} (p : x = y) : f x =[p]= f y :=
match p with
|eq_refl => eq_refl
end.

Definition coerce {X F} (c : FInter F X -> X) {P} (f : forall x : X, P x) (Pc : forall x, FLift F P x -> P (c x)) (fc : forall x, f (c x) = Pc x (all F f x)) {G} (r t : TCode c G Id) (e : forall x, TInter c r x = TInter c t x) x : TLift c Pc r x (all G f x) =[e x]= TLift c Pc t x (all G f x) -> f (TInter c r x) =[e x]= f (TInter c t x).
 rewrite coerce_eq.
 rewrite coerce_eq.
 simpl.
 intros;assumption.
 exact fc.
 exact fc.
Defined.

Axiom Mu1 : forall (F G : FCode) (r t : forall {X} {c : FInter F X -> X}, TCode c G Id), Type.
Axiom c : forall F G r t, FInter F (Mu1 F G r t) -> Mu1 F G r t.
Axiom e : forall F G r t (x : FInter G (Mu1 F G r t)), TInter (c _ _ _ _) (r _ _) x = TInter (c _ _ _ _) (t _ _) x.

Axiom Mu1_ind : forall F G r t (P : Mu1 F G r t -> Type) (Pc : forall x, FLift F P x -> P (c _ _ _ _ x)) (Pe : forall x (Px : FLift G P x), TLift (c _ _ _ _) Pc (r _ _) x Px =[e _ _ _ _ x]= TLift (c _ _ _ _) Pc (t _ _) x Px) x, P x.
Axiom Mu1_ind_c : forall F G r t P Pc Pe x, Mu1_ind F G r t P Pc Pe (c _ _ _ _ x) = Pc x (all F (Mu1_ind F G r t P Pc Pe) x).
Axiom Mu1_ind_e : forall F G r t P Pc Pe x, ap (Mu1_ind F G r t P Pc Pe) (e _ _ _ _ x) = coerce (c _ _ _ _) (Mu1_ind F G r t P Pc Pe) Pc (Mu1_ind_c F G r t P Pc Pe) (r _ _) (t _ _) (e _ _ _ _) x (Pe x (all G (Mu1_ind F G r t P Pc Pe) x)).