From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBG76SHNQKGQEC2HURQY@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-x237.google.com (mail-oi0-x237.google.com [IPv6:2607:f8b0:4003:c06::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 249ce7b4 for ; Fri, 3 Aug 2018 16:13:16 +0000 (UTC) Received: by mail-oi0-x237.google.com with SMTP id u74-v6sf5072419oie.16 for ; Fri, 03 Aug 2018 09:13:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=DsnAzRcG769ygMVx6FoMrSdmjVOBDLroBBuHcW/leUE=; b=p+Q6He/S3ETw75ji0WAV+76pNjbIm26TssgNO0hr/S/LMhPjrlLEzo82QKBQq53qYI mOY/csvEBHK/LlsFzn7v4cXNV6mBJuqGQ7v+ywPYPn0QI0oeGQSRnm1CL9XbvWJlusOU VoLrax6qnGOC41lFJolRaO0gSEs+rdDp45zJaNRdJqnNJ/9qihbKabQF51KaeplGwxIT Em5PA9IegBgRUeheS8lisqc0BfxmeYkRqoriIWZViaIuvhEkW8Jwrh4DVslE7CeBz/p6 ZAntrP3jzE/6Ou7UxlgQ7MNjHc3/MK5klUTgDcoOfHbn2RQWukp2SbRbgdSwqDaBaIFe zbww== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=DsnAzRcG769ygMVx6FoMrSdmjVOBDLroBBuHcW/leUE=; b=joZQDC9I6AAChYURxp2xTHg2arrtdefwzWGrxlCy7AJyh7yCwiit9AQeqYo9xDtvcT NiT5v9TmEp0JLQeB5ZD8VhjgTP3lbbaqhJkkw7EztOHD0ZltagjDEVlapEsI9Rgpqack hFmFiPHSp/+DDDlN0HJmjSZX9dWak7MqloKnu6wqmZUqJR2DM44X+X5q+2tvzZmG1nu3 HZv5nfiCcl+eTvil07yF5ROv3EGtcCR54CtwDFKEPvEyertL+4/3Df5ZkYaEqkYlynjl eyFDIuf/hQWC7dBGt25qsMIZNUhVdWIqMQj7o9anOnQ15JV7qjZpQlGxmnUiCSy3ARmO rezg== 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: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=DsnAzRcG769ygMVx6FoMrSdmjVOBDLroBBuHcW/leUE=; b=OmivKpIbEH/LnSVQgD8E0ZEYKKaVkSNgQukCTPFGhTh7i+bNrQTXFlclx7tN3hIxzF 94N3CBM6QVLs28m+6nyaGXuxjUMFBz0sHixLi/dVlepRJCzBn3GmtdwdDch0chcSlriI nfdmekpgAvhKmuufPc077qUnPbFD3fEs/Ko4NC7ITnjSNJbsBdAw/APrN0iVOuf04wYj /K8x57N9LB8wSRHvFM3t7wcn1e0Ul0cTAQAnLMffLcxiotTAuqd0HDN1CTbt+2kD+0bC y8zOETA922m2qsefwC7GvuvWFKb9+GNLLChGGbgTieVWBIXwEf1rJNTquJx5TrYapbpH CkGg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlG/Z0Ob7uvS7X8ospnjJQPo5DcPt++g1kX/jxZLSg5wYRRqSagn IzDQW1T/6ju1FfXHHr6leLQ= X-Google-Smtp-Source: AAOMgpciqRtehfxJLICrU3glMKPBirKVWE7RaY4IAnS7WUvLgdGugmxGpAU4eLM+uYcMVozrBk8Tng== X-Received: by 2002:aca:4787:: with SMTP id u129-v6mr222369oia.4.1533312795461; Fri, 03 Aug 2018 09:13:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4697:: with SMTP id k23-v6ls1295820oic.10.gmail; Fri, 03 Aug 2018 09:13:15 -0700 (PDT) X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr220633oih.7.1533312795058; Fri, 03 Aug 2018 09:13:15 -0700 (PDT) Date: Fri, 3 Aug 2018 09:13:14 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] TOWARDS A DIRECTED HOMOTOPY TYPE THEORY MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_687_910665289.1533312794570" 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_687_910665289.1533312794570 Content-Type: multipart/alternative; boundary="----=_Part_688_590245327.1533312794570" ------=_Part_688_590245327.1533312794570 Content-Type: text/plain; charset="UTF-8" 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_688_590245327.1533312794570 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
A preprint has appeared on the arXiv outlining a directed = HoTT by Paige Randall North.=C2=A0

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.=C2=A0
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 &= 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_688_590245327.1533312794570-- ------=_Part_687_910665289.1533312794570--