Conversation

Conversation

Notices

バツ子（痛いの痛いの飛んでけ;; (shmibs@tomo.airen-no-jikken.icu)'s status on Friday, 26-Mar-2021 00:19:32 JST バツ子（痛いの痛いの飛んでけ;;
in reply to
@nik @chj0 @a_breakin_glass it's like oop but without the gross and with more homo https://en.wikipedia.org/wiki/Homotopy_type_theory
In conversation Friday, 26-Mar-2021 00:19:32 JST from tomo.airen-no-jikken.icu permalink
Attachments
1. Domain not in remote thumbnail source whitelist: upload.wikimedia.org
  
  Homotopy type theory
  
  In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. This includes, among other lines of work, the construction of homotopical and higher-categorical models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and higher category theory; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants. There is a large overlap between the work referred to as homotopy type theory, and as the univalent foundations project. Although neither is precisely delineated, and the terms are sometimes used interchangeably, the choice of usage also sometimes corresponds to differences in viewpoint and emphasis. As such, this article may not represent the views of all researchers in the fields equally. This kind of variability...
- nikki (nik@letsalllovela.in)'s status on Friday, 26-Mar-2021 00:19:33 JST nikki
  in reply to
  - ✨ rock worshipper ????
  - chaotic avocado goblin
  @chj0 @a_breakin_glass >types of typesthis just sounds like oop to me
  
  In conversation Friday, 26-Mar-2021 00:19:33 JST permalink
- ✨ rock worshipper ???? (chj0@udongein.xyz)'s status on Friday, 26-Mar-2021 00:19:42 JST ✨ rock worshipper ????
  in reply to
  - chaotic avocado goblin
  @a_breakin_glass well, functions that operate on kinds (that is, types of types)
  
  In conversation Friday, 26-Mar-2021 00:19:42 JST permalink
- chaotic avocado goblin (a_breakin_glass@chaos.social)'s status on Friday, 26-Mar-2021 00:19:53 JST chaotic avocado goblin
  in reply to
  - ✨ rock worshipper ????
  @chj0 what're kind level functions, they sound useful
  
  In conversation Friday, 26-Mar-2021 00:19:53 JST permalink
- ✨ rock worshipper ???? (chj0@udongein.xyz)'s status on Friday, 26-Mar-2021 00:19:54 JST ✨ rock worshipper ????
  
  ever just write haskell so cursed you start needing not type-level functions, but *kind-level functions*
  
  In conversation Friday, 26-Mar-2021 00:19:54 JST permalink

Public

Notices

Feeds