*[HoTT] 1D Mu Type@ 2018-08-18 21:30 Corlin Fardal2018-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 Type2018-08-18 21:30 [HoTT] 1D Mu Type Corlin Fardal@ 2018-08-21 11:12 ` Niels van der Weide2018-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 Type2018-08-21 11:12 ` [HoTT] " Niels van der Weide@ 2018-08-21 11:20 ` András Kovács0 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 Type2018-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 Fardal2018-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 Type2018-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 Fardal2018-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 Type2018-08-22 1:49 ` Corlin Fardal@ 2018-08-22 13:05 ` András Kovács0 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 Type2018-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 Fardal3 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).