Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] 1D Mu Type
@ 2018-08-18 21:30 Corlin Fardal
  2018-08-21 11:12 ` [HoTT] " Niels van der Weide
                   ` (3 more replies)
  0 siblings, 4 replies; 7+ messages in thread
From: Corlin Fardal @ 2018-08-18 21:30 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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)).

^ permalink raw reply	[flat|nested] 7+ messages in thread

* [HoTT] Re: 1D Mu Type
  2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal
@ 2018-08-21 11:12 ` Niels van der Weide
  2018-08-21 11:20   ` András Kovács
  2018-08-22  1:49 ` Corlin Fardal
                   ` (2 subsequent siblings)
  3 siblings, 1 reply; 7+ messages in thread
From: Niels van der Weide @ 2018-08-21 11:12 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Looks interesting!
 

> 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.

I think this is might be a special case of the work by Kaposi/Kovacs on 
HIITs. See
http://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf
They gave a syntax allowing both higher paths and function types.

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.

In addition, see the paper 'Quotient Inductive Inductive Types' by 
Altenkrich, Capriotti, Dijkstra, Kraus and Forsberg. Not all HITs are 
constructible as quotients, because that would require AC. This is because 
function types are added to the syntax. Section 9.1 in Lumsdaine&Shulman's 
Semantics of Higher Inductive Types also gives a counter example. Again 
note that they use a function type in the constructor sup.

On Saturday, August 18, 2018 at 11:30:53 PM UTC+2, Corlin Fardal wrote:
>
> 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: 5581 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* [HoTT] Re: 1D Mu Type
  2018-08-21 11:12 ` [HoTT] " Niels van der Weide
@ 2018-08-21 11:20   ` András Kovács
  0 siblings, 0 replies; 7+ messages in thread
From: András Kovács @ 2018-08-21 11:20 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Hi,

Corlin Fardal: I've looked at the Agda version, it seems fine to me, but I 
think it's a bit more complicated than necessary. In particular, there's no 
need to parametrize TCode with an F-algebra. I wrote a version of my own 
here 
<https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/Functor1HIT.agda>
 with this change and a bunch of other stylistic changes.

You might be interested in this paper 
<https://pdfs.semanticscholar.org/6c81/a5233174e227d2d34270e1bdc15aae458df7.pdf>
 and demo implementation 
<https://bitbucket.org/akaposi/elims/src/dfa285fa6ba105b9cb1b9d9cc0601b239561f2d4/haskell/elims-demo/> about 
syntax and induction for higher inductive-inductive types (HIIT), which 
covers the current cases. Now, the formalization of this HIIT syntax is 
pretty heavyweight, but the general approach can be scaled back to 1-HITs, 
and then it becomes quite nice and straightforward to formalize in plain 
Agda, which I have here 
<https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/Simple1HIT.agda>. 
It's moderately more general than your 1-HITs (e.g. it includes W-types), 
and it can be formalized without function extensionality. 

András Kovács

On Tuesday, August 21, 2018 at 1:12:01 PM UTC+2, Niels van der Weide wrote:
>
> Looks interesting!
>  
>
>> 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.
>
> I think this is might be a special case of the work by Kaposi/Kovacs on 
> HIITs. See
>
> http://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf
> They gave a syntax allowing both higher paths and function types.
>
> 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.
>
> In addition, see the paper 'Quotient Inductive Inductive Types' by 
> Altenkrich, Capriotti, Dijkstra, Kraus and Forsberg. Not all HITs are 
> constructible as quotients, because that would require AC. This is because 
> function types are added to the syntax. Section 9.1 in Lumsdaine&Shulman's 
> Semantics of Higher Inductive Types also gives a counter example. Again 
> note that they use a function type in the constructor sup.
>
> On Saturday, August 18, 2018 at 11:30:53 PM UTC+2, Corlin Fardal wrote:
>>
>> 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: 9458 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* [HoTT] Re: 1D Mu Type
  2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal
  2018-08-21 11:12 ` [HoTT] " Niels van der Weide
@ 2018-08-22  1:49 ` Corlin Fardal
  2018-08-22 13:05   ` András Kovács
  2018-08-22  2:27 ` Corlin Fardal
  2018-08-22 23:54 ` Corlin Fardal
  3 siblings, 1 reply; 7+ messages in thread
From: Corlin Fardal @ 2018-08-22  1:49 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I’m pretty sure I had actually read the HIITs paper before, but I’d 
completely forgotten about it. Reading back through it it’s kind of amazing 
that I had, considering how much it manages to do very simply. I’d also 
read the QIITs paper, but, like I did with the IITs paper, gotten lost in 
the category-theoretical brushes, and ended up missing the fact that a 
quotient construction would require AC, though I'm not entirely surprised 
by that, I kind of figured it might. I did further know about the 
construction by Lumsdaine and Shulman, but I wasn't entirely certain if 
that applied to my construction, it's been a while since I've read that 
section of the paper, but as far as I can recall they didn't provide the 
actual definition of the HIT, so while I knew that it would be impossible 
to construct any HIT from quotients, I thought that the subset I had 
created a Mu type for might still be constructible, and not contain their 
HIT.

I have a few questions/comments about Kovács' version. First of all, is the 
Empty constructor necessary? It seems like we could replace it with Const 
empty, and replace exfalso with a lifted function. Additionally I'm kind of 
struggling to understand what the path algebra in the definition of Section 
is actually doing, is there a simple explanation? Also, though this doesn't 
really matter, why is the path 
algebra on the left side of the equation, instead of the right? It feels 
like if they're meant to be computation rules, it should compute from the 
left down to the right, and because of that it
feels like it ought to go from the simple application of induction to the 
path, down to a more complex expression. Additionally, as one last little 
nitpick, my name's Fardal not Fardar, as
comment at the top of the file says, though that really doesn't matter 
much. However, despite all of my nitpicks/confusions, I really like your 
version of it. The reformulation of the 
lambda term feels obvious but clever, and I'm kind of mad at myself for not coming 
up with it, seeing as one of the problems I was having was defining a 
quotient type in my version. I 
also like the connection made between the all function and the coerce 
function, I didn't realize the connection there, as, at the very least, the 
two functions needed to finish the 
computation rules. In general I like the method of building from the 
algebras to the displayed algebras to the sections, it gives the Mu type at 
the end a very nice definition. The names
of the sections sound algebraic, but I'm actually not quite sure what they 
mean. I mean, I know what an algebra is, I'm relatively well versed in the 
categorical semantics of at least
simple inductive types, but what are displayed algebras, or displayed 
algebra sections? Displayed algebras seem to have at least some connection 
to the fibred algebras of the Higher
Inductive Types as Homotopy-Initial Algebras paper, and I have some idea of 
what sections are, but is there anything deeper that I don't know about?

Now, if you'll excuse me, I'm going to go mess around with the HIIT paper's 
system and Kovác's version of my system to see if I can't understand both 
of them more, along with HITs
in general.

-- 
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: 5537 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* [HoTT] Re: 1D Mu Type
  2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal
  2018-08-21 11:12 ` [HoTT] " Niels van der Weide
  2018-08-22  1:49 ` Corlin Fardal
@ 2018-08-22  2:27 ` Corlin Fardal
  2018-08-22 23:54 ` Corlin Fardal
  3 siblings, 0 replies; 7+ messages in thread
From: Corlin Fardal @ 2018-08-22  2:27 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I’m pretty sure I had actually read the HIITs paper before, but I’d 
completely forgotten about it. Reading back through it it’s kind of amazing 
that I had, considering how much it manages to do very simply. I’d also 
read the QIITs paper, but, like I did with the IITs paper, gotten lost in 
the category-theoretical brushes, and ended up missing the fact that a 
quotient construction would require AC, though I'm not entirely surprised 
by that, I kind of figured it might. I did further know about the 
construction by Lumsdaine and Shulman, but I wasn't entirely certain if 
that applied to my construction, it's been a while since I've read that 
section of the paper, but as far as I can recall they didn't provide the 
actual definition of the HIT, so while I knew that it would be impossible 
to construct any HIT from quotients, I thought that the subset I had 
created a Mu type for might still be constructible, and not contain their 
HIT.

I have a few questions/comments about Kovács' version. First of all, is the 
Empty constructor necessary? It seems like we could replace it with Const 
empty, and replace exfalso with a lifted function. Additionally I'm kind of 
struggling to understand what the path algebra in the definition of Section 
is actually doing, is there a simple explanation? Also, though this doesn't 
really matter, why is the path 
algebra on the left side of the equation, instead of the right? It feels 
like the computation rules essentially define induction, so it feels like 
the left side should say "this is the application
of the function," and the right should say "this is the value of that 
application". Additionally, as one last little nitpick, my name's Fardal 
not Fardar, as thecomment at the top of the file 
says, though that really doesn't matter much. However, despite all of my 
nitpicks/confusions, I really like your version of it. The reformulation of 
the lambda term feels obvious but 
clever, and I'm kind of mad at myself for not coming up with it, seeing as 
one of the problems I was having was defining a quotient type in my 
version. I also like the connection made 
between the all function and the coerce function, I didn't realize the 
connection there, as, at the very least, the two functions needed to finish 
the computation rules. In general I like the
method of building from the algebras to the displayed algebras to the 
sections, it gives the Mu type at the end a very nice definition. The names of 
the sections sound algebraic, but I'm
actually not quite sure what they mean. I mean, I know what an algebra is, 
I'm relatively well versed in the categorical semantics of at least simple 
inductive types, but what are 
displayed algebras, or displayed algebra sections? Displayed algebras seem 
to have at least some connection to the fibred algebras of the Higher Inductive 
Types as Homotopy-Initial 
Algebras paper, and I have some idea of what sections are, but is there 
anything deeper that I don't know about?

Now, if you'll excuse me, I'm going to go mess around with the HIIT paper's 
system and Kovác's version of my system to see if I can't understand both 
of them more, along with HITs
in general.

-- 
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: 5965 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* Re: [HoTT] Re: 1D Mu Type
  2018-08-22  1:49 ` Corlin Fardal
@ 2018-08-22 13:05   ` András Kovács
  0 siblings, 0 replies; 7+ messages in thread
From: András Kovács @ 2018-08-22 13:05 UTC (permalink / raw)
  To: Corlin Fardal; +Cc: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 6428 bytes --]

>
> my name's Fardal not Fardar


Sorry, fixed it.

First of all, is the Empty constructor necessary?


Fair point, it isn't necessary, I removed it now.

 what the path algebra in the definition of Section is actually doing, is
> there a simple explanation? Also, though this doesn't really matter, why is
> the path
> algebra on the left side of the equation, instead of the right?


The last component of Section is just the weak (propositional) beta rule
for path constructors. If every point computation rule held definitionally,
then the path beta would be simply
(apd (Fˢ Id Xˢ) (paths gx) ≡ pathsᴰ gx (Fˢ g Xˢ gx))), which has the form
we usually see when people use HITs (with definitional point beta). Since
path beta rules are generally only well-typed up to point beta rules, we
need to refer to Tmˢ t and Tmˢ u to make it well-typed, so the left side is
wrapped in an extra composition. It's an arbitrary choice whether to
compose with point beta rules on the left side of the equation or the right
side, since the two versions are equivalent.

The names
> of the sections sound algebraic, but I'm actually not quite sure what they
> mean


It follows the terminology we use in the followup draft
<https://github.com/AndrasKovacs/misc-stuff/blob/master/publications/ConstructingQIITs-draft.pdf>
to
the HIIT stuff. In the HIIT paper we used "constructors", "motives/methods"
and "eliminators", but the new terminology is much better.  I think Mike
Shulman previously used the terms "algebra", "dependent algebra", and
"dependent algebra section". We use "displayed" instead of "dependent"
because displayed algebras generalize Ahrens and Lumsdaine's displayed
categories, in a rather precise way.

In general, semantics for a inductive types should include constructing a
category of algebras for each syntactic declaration, where algebra
homomorphisms are the morphisms. However, if we only have a category, we
can only talk about initiality (unique recursion), but not about induction,
because that needs a notion of dependent object/family/fibration. So we
need to have a category with a notion of dependent objects. In the draft
paper we use CwF (category with families) where displayed algebras and
sections form the "F" part, but there are probably other workable choices
as well.

Corlin Fardal <fardalcorlin@gmail.com> ezt írta (időpont: 2018. aug. 22.,
Sze, 3:49):

> I’m pretty sure I had actually read the HIITs paper before, but I’d
> completely forgotten about it. Reading back through it it’s kind of amazing
> that I had, considering how much it manages to do very simply. I’d also
> read the QIITs paper, but, like I did with the IITs paper, gotten lost in
> the category-theoretical brushes, and ended up missing the fact that a
> quotient construction would require AC, though I'm not entirely surprised
> by that, I kind of figured it might. I did further know about the
> construction by Lumsdaine and Shulman, but I wasn't entirely certain if
> that applied to my construction, it's been a while since I've read that
> section of the paper, but as far as I can recall they didn't provide the
> actual definition of the HIT, so while I knew that it would be impossible
> to construct any HIT from quotients, I thought that the subset I had
> created a Mu type for might still be constructible, and not contain their
> HIT.
>
> I have a few questions/comments about Kovács' version. First of all, is
> the Empty constructor necessary? It seems like we could replace it with
> Const empty, and replace exfalso with a lifted function. Additionally I'm
> kind of
> struggling to understand what the path algebra in the definition of
> Section is actually doing, is there a simple explanation? Also, though this
> doesn't really matter, why is the path
> algebra on the left side of the equation, instead of the right? It feels
> like if they're meant to be computation rules, it should compute from the
> left down to the right, and because of that it
> feels like it ought to go from the simple application of induction to the
> path, down to a more complex expression. Additionally, as one last little
> nitpick, my name's Fardal not Fardar, as
> comment at the top of the file says, though that really doesn't matter
> much. However, despite all of my nitpicks/confusions, I really like your
> version of it. The reformulation of the
> lambda term feels obvious but clever, and I'm kind of mad at myself for
> not coming up with it, seeing as one of the problems I was having was
> defining a quotient type in my version. I
> also like the connection made between the all function and the coerce
> function, I didn't realize the connection there, as, at the very least,
> the two functions needed to finish the
> computation rules. In general I like the method of building from the
> algebras to the displayed algebras to the sections, it gives the Mu type
> at the end a very nice definition. The names
> of the sections sound algebraic, but I'm actually not quite sure what they
> mean. I mean, I know what an algebra is, I'm relatively well versed in the
> categorical semantics of at least
> simple inductive types, but what are displayed algebras, or displayed
> algebra sections? Displayed algebras seem to have at least some connection
> to the fibred algebras of the Higher
> Inductive Types as Homotopy-Initial Algebras paper, and I have some idea
> of what sections are, but is there anything deeper that I don't know about?
>
> Now, if you'll excuse me, I'm going to go mess around with the HIIT
> paper's system and Kovác's version of my system to see if I can't
> understand both of them more, along with HITs
> in general.
>
> --
> 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.
>

-- 
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 #2: Type: text/html, Size: 10447 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

* [HoTT] Re: 1D Mu Type
  2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal
                   ` (2 preceding siblings ...)
  2018-08-22  2:27 ` Corlin Fardal
@ 2018-08-22 23:54 ` Corlin Fardal
  3 siblings, 0 replies; 7+ messages in thread
From: Corlin Fardal @ 2018-08-22 23:54 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I could tell that the path algebra was doing something similar to my 
original coerce function, I was just curious how exactly it worked, with 
perhaps a breakdown of what each part is doing, and how you even came up 
with the term in the first place, it seems non-obvious to me, to say the 
very least. Also, I knew that the choice of putting it on the left or the 
right was equivalent, I tried to say as much, but seeing as it aligns with 
what you do in the HIITs paper, I was curious if there was a particular 
reason you seem to prefer the left over the right.

-- 
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: 1051 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

end of thread, other threads:[~2018-08-22 23:55 UTC | newest]

Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal
2018-08-21 11:12 ` [HoTT] " Niels van der Weide
2018-08-21 11:20   ` András Kovács
2018-08-22  1:49 ` Corlin Fardal
2018-08-22 13:05   ` András Kovács
2018-08-22  2:27 ` Corlin Fardal
2018-08-22 23:54 ` Corlin Fardal

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).