From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB26PSLNQKGQEWEWO3LY@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-oi0-x23e.google.com (mail-oi0-x23e.google.com [IPv6:2607:f8b0:4003:c06::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f9bbfd3f for ; Fri, 3 Aug 2018 19:07:24 +0000 (UTC) Received: by mail-oi0-x23e.google.com with SMTP id j5-v6sf5535643oiw.13 for ; Fri, 03 Aug 2018 12:07:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=GA+2id2OYK6GslUDIbU8zPwVBsRTOnvkBE092+LvWjs=; b=haXw07IAtvdF6IOJTwdB3EhrL1ITTI/x4IoQNRuqqbNFomDvPn3pYcqq8KoT/LHY5Z wu2+9vSwLhgnCgjr/Zz/SlxOszkG4VnFeuizgd4UF8CfqjyHUxcpfWtqZl/ljzLtg1Zu aXy+gHMNWlEyzmbLJUGSdd4mgR0B2P0HbaSMhLqsuKNLXif4F0sx22OIG8bXnUYboyjp nV24XP8tYo1RwgSgK6Wdf8M2FfJ9SjpjxKLNUn5rI+lmOgtIwLZl0oCRI54cfIyuLzaI MBwdvk4mygx3ToNfnp5L0iSkW4By3l68ObxpZPTxhefPrFKVCxSO16tUnvDQyhfBFPjh AHJw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=GA+2id2OYK6GslUDIbU8zPwVBsRTOnvkBE092+LvWjs=; b=BWDZxInlGLX5fSTQtnK6cvA9+gcGsSvpbdeTjRg5M5L4d2/kdUpDmZiSMRZ8JJgdGD b03ahqal8ep5M3/Exdt8zhPrZh6rnaY2ttG1DpV5/jyQDgSr8C0xtQybJO7QUPH6t7Su P0KEjzbl2NRXxpvETgtuWW6O6TVebnXihawtOGYCJaSr7RF8mFp1s0Us7FcplN4P5zxw 1ioYDWExUaoo8yo1pK/pU/VhkeWs84ROnthyYA/zt8O5enY5KVPgIqtHo3TOLcQsJj5L I73b3HhOinXHBCyO+rL+faC8TIdKpov7uIcqdtk0uM9ojBdT/Gs79uFvgXluMrzLMV9u NfPQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=GA+2id2OYK6GslUDIbU8zPwVBsRTOnvkBE092+LvWjs=; b=BI8ocUiRD7P4HkI91ZQ+NFtHCln4aZCLXQbwoSBCNCuuImVhCVjuqj3dJdyikdWDZU Gd05Cp+uJoAAwaskXzFNNNpiX0DeVXtUxjjiOg8Lcdgqm3UFUFOur3SK57asbyCvszF8 dsx5PU8A9FWoNsN7M8Lv2Ttb0B9MPA5hbzofm0uKcIX9eNxvpniPHDB/xGHYo3YrQJ+1 oiw0tjRvFkJaBXmuF6DCeizkV5WI3vHl9BbkamQrofS47ZO/y8WzUIAOlZ/m86j1R9dj 0h7V48yCaz7RDXTp9VbEed0RnTbVw2ZjuK6z2wDDUWNoPMrUgqrD3LFls+2MeL/mJe6+ 7eDA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEu78yQqKnv9k8ArX3SEH+QzPrioZTdrizMrMZQjX1G6Fp9A6FH 5OgjATCXh3zhm1uhtFTLyxo= X-Google-Smtp-Source: AAOMgpd/geYuRuA7t0tfEJM/hYkhwnoDETS5Pv1JTmM2N2J2w4J+MsEaY6+PNtU8OI82XrY3Ptm/Tg== X-Received: by 2002:aca:75c9:: with SMTP id q192-v6mr237205oic.3.1533323243778; Fri, 03 Aug 2018 12:07:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:6709:: with SMTP id z9-v6ls1520876oix.1.gmail; Fri, 03 Aug 2018 12:07:23 -0700 (PDT) X-Received: by 2002:aca:2b06:: with SMTP id i6-v6mr232343oik.0.1533323243276; Fri, 03 Aug 2018 12:07:23 -0700 (PDT) Date: Fri, 3 Aug 2018 12:07:22 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: TOWARDS A DIRECTED HOMOTOPY TYPE THEORY MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_765_347397416.1533323242703" X-Original-Sender: alizter@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_765_347397416.1533323242703 Content-Type: multipart/alternative; boundary="----=_Part_766_314918863.1533323242703" ------=_Part_766_314918863.1533323242703 Content-Type: text/plain; charset="UTF-8" Just realised I didn't include a link: https://arxiv.org/pdf/1807.10566.pdf On Friday, 3 August 2018 17:13:14 UTC+1, Ali Caglayan wrote: > > A preprint has appeared on the arXiv outlining a directed HoTT by Paige > Randall North. > > Just from skimming so far it appears to be a standard Martin-Lof with a > core, op and hom-type. > > The core type gives the set of objects of a type (I suppose types are now > categories of sorts). The op type gives the opposite category, then the hom > type is the directed path type. > > As far as I can tell this type theory has semantics in Cat. > > I would be interested on others thoughts on 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. ------=_Part_766_314918863.1533323242703 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Just realised I didn't include a link:

<= div>https://arxiv.org/pdf/1807.10566.pdf

On Friday, 3 August 2018 17= :13:14 UTC+1, Ali Caglayan wrote:
A preprint has appeared on the arXiv outlining a dir= ected HoTT by Paige Randall North.=C2=A0

Just from skimm= ing so far it appears to be a standard Martin-Lof with a core, op and hom-t= ype.

The core type gives the set of objects of a t= ype (I suppose types are now categories of sorts). The op type gives the op= posite category, then the hom type is the directed path type.=C2=A0

As far as I can tell this type theory has semantics in Ca= t.

I would be interested on others thoughts on thi= s.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_766_314918863.1533323242703-- ------=_Part_765_347397416.1533323242703--