Algebra operations #1428

andreaslyn · 2021-03-25T19:06:02Z

Started work on algebra operations

Added Finite/FinSeq.v

Make some definitions monomorphic to fix universe blowup in Finite/FinNat.v

andreaslyn · 2021-03-25T19:06:56Z

theories/Algebra/Universal/Operation.v

+(** Functions [head_dom'] and [head_dom] are used to get the first
+    element of a nonempty operation domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition head_dom' {σ} (A : Carriers σ) (n : nat)


I am making certain definitions monomorphic to avoid unverse blowup.

andreaslyn · 2021-03-25T19:07:46Z

theories/Spaces/Finite/Fin.v

@@ -112,14 +112,14 @@ Proof.
    + rewrite path_fin_fsucc_incl, path_nat_fin_incl.
      apply IHn.
    + reflexivity.
-Qed.
+Defined.


I need the computation for operation_curry.

That's curious, since it's a path in nat. Is it not possible to just use the fact that nat is a set?

It is because I want the definitional equality from operation_curry: https://github.com/HoTT/HoTT/blob/9e8e09146747077eb81c6f152bc5f04b4d7cd5f5/theories/Algebra/Universal/Operation.v#L141

andreaslyn · 2021-03-25T19:08:41Z

theories/Spaces/Finite/FinNat.v

@@ -79,7 +79,8 @@ Proof.
                   (hset_path2 1 (@path_succ_finnat n u u.2)) idpath).
 Defined.

-Definition is_bounded_fin_to_nat {n} (k : Fin n) : fin_to_nat k < n.
+Monomorphic Definition is_bounded_fin_to_nat {n} (k : Fin n)


Monomorphic to avoid universe blowup

andreaslyn · 2021-03-25T19:09:22Z

theories/Spaces/Finite/Vect.v

+(** Finite-dimensional vector. Note that the induction principle
+    [vect_ind] uses funext and does not compute. *)
+
+Definition Vect (n : nat) (A : Type) : Type := Fin n -> A.


I am not sure whether vector is a good name for this.

Well, it's at least a traditional name in dependent type theory, right? Although I guess it's more common to define as an indexed family than as a function type. But yeah, it might be confusing if we start also doing linear algebra. (-: Any other suggestions?

I'm curious why you decided to define them this way rather than as an inductive family? It seems like the latter would use less funext, for one thing.

I think that Vect is a traditional name in dependent type theory, but perhaps not suitable here. An alternative is FinSeq for finite sequence.

In the multi-sorted universal algebra that I am developing, this type occurs as the of sorts for the domain of finitary operations: https://github.com/HoTT/HoTT/blob/9e8e09146747077eb81c6f152bc5f04b4d7cd5f5/theories/Algebra/Universal/Operation.v#L77

In my initial approach I defined the inductive family and proved the two equivalent, but I do not need the inductive family, so I decided to leave it out.

I use funext to derive the induction principle for the type, which I just included for completeness. I do not expect to need that for universal algebra.

FinSeq could be good. Why is this definition preferable to the inductive one?

I think the inductive family is often preferable, but in my particular case I need this one to instantiate the SymbolTypeOf record: https://github.com/HoTT/HoTT/blob/bce95e43fe3407706ac0eae1bd9ddaf7d42fb2b9/theories/Algebra/Universal/Algebra.v#L23 when Arity is Fin n.

I am fine with having both notions of FinSeq. The "default" inductive definition in HoTT.Spaces.FinSeq and this one in HoTT.Spaces.Finite.FinSeq. What do you think?

andreaslyn · 2021-03-25T19:12:38Z

theories/Spaces/Finite/Vect.v

+(** A non-empty vector is the [vcons] of its head and tail,
+    [path_expand_vcons'] and [path_expand_vcons]. *)
+
+Lemma path_expand_vcons' {A : Type} (n : nat)


The remaining lemmas are here to prove vect_ind. I do not think that I will need it, but I formalised vect_ind for completeness.

mikeshulman · 2021-03-26T23:18:30Z

Sure. No need to add the inductive one until someone needs or wants it.

…

On Fri, Mar 26, 2021 at 4:01 PM Andreas Lynge ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In theories/Spaces/Finite/Vect.v <#1428 (comment)>: > @@ -0,0 +1,212 @@ +Require Import + HoTT.Basics + HoTT.Types + HoTT.HSet + HoTT.DProp + HoTT.Spaces.Finite.Fin + HoTT.Spaces.Finite.FinInduction + HoTT.Spaces.Nat. + +(** Finite-dimensional vector. Note that the induction principle + [vect_ind] uses funext and does not compute. *) + +Definition Vect (n : nat) (A : Type) : Type := Fin n -> A. I think the inductive family is often preferable, but in my particular case I need this one to instantiate the SymbolTypeOf record: https://github.com/HoTT/HoTT/blob/bce95e43fe3407706ac0eae1bd9ddaf7d42fb2b9/theories/Algebra/Universal/Algebra.v#L23 when Arity is Fin n. I am fine with having both notions of FinSeq. The "default" inductive definition in HoTT.Spaces.FinSeq and this one in HoTT.Spaces.Finite.FinSeq. What do you think? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1428 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE53SAGBW4ZKTBFSJM6CSTTFUG6PANCNFSM4ZZ6MGMQ> .

andreaslyn · 2021-03-31T22:25:04Z

I have rebased and changed Vect to FinSeq.

Alizter · 2021-04-02T16:42:32Z

The universe issues here are interesting. We can fix some issues by changing Fin in Finite/Fin.v to the following:

Fixpoint Fin (n : nat) : Type0
  := match n with
       | 0 => Empty
       | S n => Fin n + Unit
     end.

It makes sense to stick it in the lowest universe, just like we do with nat. So Fin doesn't depend on universes.

This let's us reduce the universes in FinSeq as a result. In general I would opt for:

Definition FinSeq@{u} (n : nat) (A : Type@{u}) : Type@{u} := Fin n -> A.

This means that FinSeq only has one universe.

This should reduce some of the blowup I observed.

andreaslyn · 2021-04-02T18:09:08Z

Good idea. I have added those changes.

Started work on algebra operations Added Finite.Vect Make some definitions monomorphic to fix universe blowup in Finite.FinNat

Put Fin in lowest universe and 1 universe for FinSeq.

andreaslyn · 2021-04-05T21:18:09Z

Are we OK with merging this?

mikeshulman · 2021-04-05T21:20:26Z

Looks fine to me.

andreaslyn commented Mar 25, 2021

View reviewed changes

andreaslyn force-pushed the infinitary-universal-algebra branch 2 times, most recently from 3fae52a to e7d9b94 Compare March 31, 2021 22:22

andreaslyn force-pushed the infinitary-universal-algebra branch from c6cac28 to da0c0a6 Compare April 2, 2021 18:11

andreaslyn added 4 commits April 5, 2021 22:21

Algebra operations

f8c8ec7

Started work on algebra operations Added Finite.Vect Make some definitions monomorphic to fix universe blowup in Finite.FinNat

New line in the end of files and typo

67be5bc

Change Vect to FinSeq

6906546

Decrease number of universes

7137029

Put Fin in lowest universe and 1 universe for FinSeq.

andreaslyn force-pushed the infinitary-universal-algebra branch from da0c0a6 to 7137029 Compare April 5, 2021 20:21

Alizter merged commit dd3c399 into HoTT:master Apr 5, 2021

andreaslyn mentioned this pull request Apr 20, 2021

Turn FinSeq into an inductive type #1467

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Algebra operations #1428

Algebra operations #1428

andreaslyn commented Mar 25, 2021 •

edited

Loading

andreaslyn Mar 25, 2021

andreaslyn Mar 25, 2021

mikeshulman Mar 26, 2021

andreaslyn Mar 26, 2021

andreaslyn Mar 25, 2021

andreaslyn Mar 25, 2021

mikeshulman Mar 26, 2021

mikeshulman Mar 26, 2021

andreaslyn Mar 26, 2021

andreaslyn Mar 26, 2021

mikeshulman Mar 26, 2021

andreaslyn Mar 26, 2021

andreaslyn Mar 25, 2021

mikeshulman commented Mar 26, 2021 via email

andreaslyn commented Mar 31, 2021

Alizter commented Apr 2, 2021

andreaslyn commented Apr 2, 2021

andreaslyn commented Apr 5, 2021

mikeshulman commented Apr 5, 2021

Algebra operations #1428

Algebra operations #1428

Conversation

andreaslyn commented Mar 25, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mikeshulman commented Mar 26, 2021 via email

andreaslyn commented Mar 31, 2021

Alizter commented Apr 2, 2021

andreaslyn commented Apr 2, 2021

andreaslyn commented Apr 5, 2021

mikeshulman commented Apr 5, 2021

andreaslyn commented Mar 25, 2021 •

edited

Loading