Description

• Title:
  The Theory of an Arbitrary Higher \(\lambda\)-Model
• Creator:
  Martínez-Rivillas, Daniel O.;
  de Queiroz, Ruy J. G. B.
• Contributor:
  Martínez-Rivillas, Daniel O. - Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil;
  de Queiroz, Ruy J. G. B. - Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil;
  Martínez-Rivillas, Daniel O. - domr@cin.ufpe.br;
  de Queiroz, Ruy J. G. B. - ruy@cin.ufpe.br
• Description:
  One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2023.06.07;
  2023.04.25
• Type:
  Other
• Language:
  English;
  eng
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;1;
  52
• Subject:
  higher lambda calculus;
  homotopic lambda model;
  Kan complex reflexive;
  higher conversion;
  homotopy type-free theory
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/47236 ;
  2449-836X;
  10.18778/0138-0680.2023.11
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  other