pith. sign in

arxiv: 2504.11225 · v2 · submitted 2025-04-15 · 💻 cs.LO · math.CT

Doctrinal Semantics of Directed First-Order Logic

Andrea Laretto , Fosco Loregian , Niccol\`o Veltri This is my paper

Pith reviewed 2026-05-22 20:44 UTC · model grok-4.3

classification 💻 cs.LO math.CT
keywords directed first-order logicdirected equalitypolaritiesrelative left adjointdirected doctrinessoundness and completenesspreorders
0
0 comments X

The pith

Directed first-order logic equips equality with direction so that types interpret as preorders.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a first-order logic in which equality is asymmetric and stands for rewrites rather than mutual implications. A syntactic polarity system marks each variable occurrence as positive, negative, or both to enforce the direction. This polarity data lets the authors characterize directed equality as a relative left adjoint, extending the classical adjoint view of equality. The logic receives categorical semantics through directed doctrines, which the authors prove sound and complete for the syntax. The classical fragment of the logic is separately shown to be complete when interpreted in preorders.

Core claim

We equip first-order logic with an asymmetric equality that behaves like a rewrite between terms and introduce a polarity system on variables to track their occurrences. Directed equality is then characterized as a relative left adjoint, with the relativeness capturing the syntactic restrictions that block symmetry. The semantics of the logic and its variances are given by directed doctrines, which are shown to be sound and complete with respect to the syntax; the classical fragment is also complete under standard preorder semantics.

What carries the argument

Directed doctrine, the categorical structure that interprets the logic, its directed equality, and the system of polarities on variables.

If this is right

  • Directed equality satisfies a universal property that respects one-way rewrites without forcing symmetry.
  • The full logic is sound and complete when interpreted in directed doctrines.
  • The classical fragment remains complete when restricted to ordinary preorder models.
  • The relative adjoint characterization isolates exactly the syntactic restrictions needed to keep equality directed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same polarity mechanism could be applied to other logical connectives to enforce directed behavior throughout a larger fragment of logic.
  • Completeness results open the possibility of using categorical constructions in directed doctrines to derive new proof rules for the syntax.
  • The separation between the directed and classical fragments suggests a modular way to add directionality only where needed without affecting ordinary reasoning.

Load-bearing premise

The syntactic polarities on variable occurrences correctly restrict the logic so that directed equality never implies its own reverse.

What would settle it

A formula provable in the directed logic that fails to hold in some model of directed doctrines, or a counterexample showing the classical fragment incomplete in preorders.

Figures

Figures reproduced from arXiv: 2504.11225 by Andrea Laretto, Fosco Loregian, Niccol\`o Veltri.

Figure 1
Figure 1. Figure 1: Intuition for syntax and preorder semantics of directed [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of directed first-order logic – types and terms. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Syntax of directed first-order logic – formulas. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Syntax of directed first-order logic – entailments. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Derived rules for polarized exponentials. [PITH_FULL_IMAGE:figures/full_fig_p027_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Derived rules for directed equality. ∆, Γ ⊢ ρ : P [Θ | ∆ | Γ] Φ ⊢ ϕ(ρ) (∃ + t ) [Θ | ∆ | Γ] Φ ⊢ ∃+x.ψ(x) ∆, Γ ⊢ ρ : P [Θ | ∆ | Γ] Φ ⊢ ∀+x.ψ(x) (∀ + t ) [Θ | ∆ | Γ] Φ ⊢ ψ(ρ) Θ, ∆ ⊢ η : N [Θ | ∆ | Γ] Φ ⊢ ϕ(η) (∃ − t ) [Θ | ∆ | Γ] Φ ⊢ ∃−x.ψ(x) Θ, ∆ ⊢ η : N [Θ | ∆ | Γ] Φ ⊢ ∀−x.ψ(x) (∀ − t ) [Θ | ∆ | Γ] Φ ⊢ ψ(η) ∆ ⊢ δ : D [Θ | ∆ | Γ] Φ ⊢ ϕ(δ, δ) (∃ ∆ t ) [Θ | ∆ | Γ] Φ ⊢ ∃∆x.ψ(x, x) ∆ ⊢ δ : D [Θ | ∆ | Γ] Φ ⊢ ∀δx… view at source ↗
Figure 7
Figure 7. Figure 7: Derived rules for quantifiers. 27 [PITH_FULL_IMAGE:figures/full_fig_p027_7.png] view at source ↗
read the original abstract

We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as preorders. The logic is equipped with a precise syntactic system of polarities, inspired by dinaturality, that keeps track of the occurrence of variables (positive/negative/both). We use this to give a characterization of directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint; intuitively, the relativeness is used to capture the syntactic restriction that avoids symmetry of equality. The semantics of this logic and its system of variances is captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax. Moreover, we prove that the classical fragment of our directed logic is complete with respect to a standard semantics in preorders.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The manuscript introduces a first-order logic with an asymmetric directed equality (interpreted as rewrites, with types as preorders) together with a syntactic polarity system (positive/negative/both, inspired by dinaturality) that tracks variable occurrences. It characterizes directed equality as a relative left adjoint to the diagonal functor, generalizing Lawvere's adjoint characterization of equality. Semantics are given by directed doctrines; the paper proves soundness and completeness of the logic with respect to these doctrines and proves completeness of the classical fragment with respect to standard preorder semantics.

Significance. If the soundness and completeness theorems hold, the work provides a coherent categorical semantics for directed logic that properly handles variances via polarities and relative adjoints. The generalization of Lawvere's equality-as-left-adjoint idea to a non-symmetric setting, together with the explicit soundness/completeness results for directed doctrines and the classical fragment, constitutes a solid contribution to categorical logic and could support further developments in directed type theory and rewriting semantics.

major comments (1)
  1. [§4.3 and Theorem 5.4] §4.3, Definition 4.12 (directed doctrine) and Theorem 5.4 (completeness): the relative-left-adjoint characterization of directed equality depends on the polarity system enforcing that only positive occurrences appear in the left-hand side of the equality; the proof sketch does not explicitly verify that the 'both' polarity case in the syntactic rules does not inadvertently allow a symmetric implication to be derived in the doctrine semantics.
minor comments (3)
  1. [§2.2] §2.2: the citation to Lawvere's original equality-as-adjoint result should include the precise reference (e.g., the 1970 paper) rather than a general mention.
  2. [§3.1] Notation in §3.1: the polarity annotations on variables are introduced with three symbols but the text occasionally re-uses the same symbol for 'both' and 'positive' in different contexts; a single consistent notation table would help.
  3. [Figure 2] Figure 2 (the commuting diagram for the relative adjunction): the arrow directions for the directed equality are visually ambiguous; adding explicit labels for the variance would improve clarity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the positive assessment of its contribution. We address the single major comment below.

read point-by-point responses

  1. Referee: [§4.3 and Theorem 5.4] §4.3, Definition 4.12 (directed doctrine) and Theorem 5.4 (completeness): the relative-left-adjoint characterization of directed equality depends on the polarity system enforcing that only positive occurrences appear in the left-hand side of the equality; the proof sketch does not explicitly verify that the 'both' polarity case in the syntactic rules does not inadvertently allow a symmetric implication to be derived in the doctrine semantics.

    Authors: We agree that the proof sketch of Theorem 5.4 is brief and does not contain an explicit case analysis for the 'both' polarity. The syntactic polarity rules (introduced in §3 and used in the definition of directed equality) restrict the formation of directed equalities so that a 'both' occurrence on the left-hand side is only admitted when the surrounding context already enforces the directed variance; the relative-left-adjoint property in a directed doctrine (Definition 4.12) is stated with respect to the subcategory of morphisms that respect the declared polarities, which excludes the reversal needed for symmetry. Nevertheless, to make this fully transparent we will expand the proof of Theorem 5.4 with a dedicated paragraph that checks the 'both' case directly in the doctrine semantics and confirms that no symmetric implication becomes derivable. This is a clarification of the existing argument rather than a change to the theorems themselves. revision: yes

Circularity Check

0 steps flagged

No significant circularity; standard soundness/completeness for new syntax/semantics

full rationale

The paper defines a directed first-order logic with a polarity system and directed doctrines, then establishes soundness and completeness theorems relative to the syntax and a preorder semantics for the classical fragment. These are independent categorical constructions and proofs that do not reduce by definition or self-citation to their own inputs. The generalization of Lawvere's adjoint characterization uses an external reference and introduces new relative-adjoint machinery without circular reduction. No fitted parameters, self-definitional equalities, or load-bearing self-citations appear in the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

Limited information available from abstract only; paper introduces new entities while relying on standard background from category theory.

axioms (1)
  • standard math Standard axioms of category theory including adjunctions and doctrines
    Invoked to characterize directed equality as relative left adjoint and to define directed doctrines for semantics.
invented entities (2)
  • directed doctrine no independent evidence
    purpose: Captures semantics of the directed logic and its system of variances
    New categorical structure introduced to provide sound and complete interpretation of the logic.
  • directed equality as relative left adjoint no independent evidence
    purpose: Provides asymmetric characterization of equality avoiding symmetry
    Core generalization of Lawvere's equality idea tailored to the directed setting.

pith-pipeline@v0.9.0 · 5683 in / 1319 out tokens · 49222 ms · 2026-05-22T20:44:02.447073+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages · 2 internal anchors

  1. [1]

    Mathematical Structures in Computer Scien ce pp

    Ahrens, B., North, P.R., van der Weide, N.: Bicategorica l type theory: seman- tics and syntax. Mathematical Structures in Computer Scien ce pp. 1–45 (Oct 2023). https://doi.org/10.1017/S0960129523000312

    work page doi:10.1017/s0960129523000312 2023

  2. [2]

    https://doi.org/10.48550/arXiv.2410.19520

    Altenkirch, T., Neumann, J.: Synthetic 1-Categories in Directed Type Theory (Oct 2024). https://doi.org/10.48550/arXiv.2410.19520

    work page doi:10.48550/arxiv.2410.19520 2024

  3. [3]

    Journal of Pure and Applied Algebra 228(9), 107676 (Sep 2024)

    Arkor, N., McDermott, D.: The formal theory of relative m onads. Journal of Pure and Applied Algebra 228(9), 107676 (Sep 2024). https://doi.org/10.1016/j.jpaa. 2024.107676

    work page doi:10.1016/j.jpaa 2024

  4. [4]

    In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

    Atkey, R., Ghani, N., Johann, P.: A relationally paramet ric model of dependent type theory. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 503–515. POPL ’14, Association for Computin g Machinery, New York, NY, USA (Jan 2014). https://doi.org/10.1145/2535838.2535852

    work page doi:10.1145/2535838.2535852 2014

  5. [5]

    url: http://dx.doi.org/10.1017/S0305004108001783

    Awodey, S., Warren, M.A.: Homotopy theoretic models of i dentity types. Math- ematical Proceedings of the Cambridge Philosophical Socie ty 146(1), 45–55 (2009). https://doi.org/10.1017/S0305004108001783

    work page doi:10.1017/s0305004108001783 2009

  6. [6]

    : Functorial polymorphism

    Bainbridge, E.S., Freyd, P.J., Scedrov, A., Scott, P.J. : Functorial polymorphism. Theoretical Computer Science 70(1), 35–64 (Jan 1990). https://doi.org/10.1016/0304-397 5(90)90151-7

    work page doi:10.1016/0304-397 1990

  7. [7]

    Proceedings of the London Mathe- matical Society 102(2), 370–394 (Oct 2010)

    van den Berg, B., Garner, R.: Types are weak ω-groupoids. Proceedings of the London Mathe- matical Society 102(2), 370–394 (Oct 2010). https://doi.org/10.1112/plms/p dq026

    work page doi:10.1112/plms/p 2010

  8. [8]

    https://doi.org/10.1145/203095.203096

    Castagna, G.: Covariance and contravariance: conflict w ithout a cause 17(3), 431–447. https://doi.org/10.1145/203095.203096

    work page doi:10.1145/203095.203096

  9. [9]

    In: 30th International Conference on Types for Proofs and Programs TYPES 2024–Abst racts

    Chu, F., Mangel, E., North, P.R.: A directed type theory f or 1-categories. In: 30th International Conference on Types for Proofs and Programs TYPES 2024–Abst racts. p. 205 (2024)

    work page 2024

  10. [10]

    Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

    Cohen, C., Coquand, T., Huber, S., M¨ ortberg, A.: Cubic al Type Theory: A Constructive Interpre- tation of the Univalence Axiom. In: Uustalu, T. (ed.) 21st In ternational Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Pr oceedings in Informatics (LIPIcs), vol. 69, pp. 5:1–5:34. Schloss Dagstuhl – Leibniz-Zentrum f ¨ ur In...

    work page doi:10.4230/lipics.types.2015.5 2015

  11. [11]

    Springer, London (2 013)

    van Dalen, D.: Logic and Structure. Springer, London (2 013). https://doi.org/10.1007/978-1-4471- 4558-5 7

    work page doi:10.1007/978-1-4471-

  12. [12]

    In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc, E., Phreilambud, Pultr, A., Street, R., Tierney, M., Swierczkowski, S

    Dubuc, E., Street, R.: Dinatural transformations. In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc, E., Phreilambud, Pultr, A., Street, R., Tierney, M., Swierczkowski, S. (eds.) Reports of 23 the Midwest Category Seminar IV. pp. 126–137. Lecture Notes in Mathematics, Springer, Berlin, Heidelberg (1970). https://doi.org/10.1007/BFb0060443

    work page doi:10.1007/bfb0060443 1970

  13. [13]

    Springer International Publishing

    Fajstrup, L., Goubault, E., Haucourt, E., Mimram, S., R aussen, M.: Directed Algebraic Topology and Concurrency. Springer International Publishing. http s://doi.org/10.1007/978-3-319-15398-8

    work page doi:10.1007/978-3-319-15398-8

  14. [14]

    In: Proceedings

    Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and va riable binding. In: Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR0015 8). pp. 193–202 (Jul 1999). https://doi.org/10.1109/LICS.1999.782615, iSSN: 1043- 6871

    work page doi:10.1109/lics.1999.782615 1999

  15. [15]

    Brookes and Michael W

    Fiore, M., Rosolini, G.: The category of cpos from a synt hetic viewpoint 6, 133–150. https://doi.org/https://doi.org/10.1016/S1571-0661(05)80165-3, mFPS XIII, Mathematical Foun- dations of Progamming Semantics, Thirteenth Annual Confer ence

    work page doi:10.1016/s1571-0661(05)80165-3

  16. [16]

    In: Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992

    Freyd, P.J., Robinson, E.P., Rosolini, G.: Functorial parametricity. In: Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS ’92), Santa Cruz, California, USA, June 22-25, 1992. pp. 444–452. IEEE C omputer Society (1992). https://doi.org/10.1109/LICS.1992.185555

    work page doi:10.1109/lics.1992.185555 1992

  17. [17]

    https://doi.org/10.48550/arXiv.2407.09146, ar Xiv.2407.09146

    Gratzer, D., Weinberger, J., Buchholtz, U.: Directed u nivalence in simplicial homotopy type theory (2024). https://doi.org/10.48550/arXiv.2407.09146, ar Xiv.2407.09146

    work page doi:10.48550/arxiv.2407.09146 2024

  18. [18]

    Springer-Verlag, Berlin, Hei- delberg (1997)

    Hofmann, M.: Extensional Constructs in Intensional Ty pe Theory. Springer-Verlag, Berlin, Hei- delberg (1997)

    work page 1997

  19. [19]

    I n: Pitts, A.M., Dyb- jer, P., Pitts, A.M., Dybjer, P

    Hofmann, M.: Syntax and Semantics of Dependent Types. I n: Pitts, A.M., Dyb- jer, P., Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, pp. 79–

    work page

  20. [20]

    https://doi.org/10.1017/CBO9780511526619.004

    Publications of the Newton Institute, Cambridge Unive rsity Press, Cambridge (1997). https://doi.org/10.1017/CBO9780511526619.004

    work page doi:10.1017/cbo9780511526619.004 1997

  21. [21]

    Oxford Univer- sity Press (2018).https://doi.org/10.1093/oso/9780198814788.001.0001

    Hofmann, M., Streicher, T.: The groupoid interpretati on of type theory. In: Sambin, G., Smith, J.M. (eds.) Twenty-five years of constructive type th eory (Venice, 1995), Oxford Logic Guides, vol. 36, pp. 83–111. Oxford Univ. Press, New Yo rk, New York (Oct 1998). https://doi.org/10.1093/oso/9780198501275.003.0008

    work page doi:10.1093/oso/9780198501275.003.0008 1995

  22. [22]

    Jacobs, B.P.F.: Categorical Logic and Type Theory, Stu dies in Logic and the Foundations of Mathematics, vol. 141. North-Holland (1999)

    work page 1999

  23. [23]

    Kapulkin, C., Lumsdaine, P.L.: The Simplicial Model of Univalent Foundations (after Voevodsky). Tech. rep. (2012). https://doi.org/10.48550/arXiv.1211.2851, arXiv:1211.2851 [math] type: article

    work page doi:10.48550/arxiv.1211.2851 2012

  24. [24]

    Laretto, A., Loregian, F., Veltri, N.: Directed equali ty with dinaturality (2024), https://arxiv.org/abs/2409.10237

    work page arXiv 2024

  25. [25]

    Laretto, A., Loregian, F., Veltri, N.: Directed equali ty for (co)end calculus (2025), available at https://iwilare.com/directed-equality-for-coend-cal culus.pdf

    work page 2025

  26. [26]

    Lawvere, F.W.: Functorial Semantics of Algebraic Theo ries. Ph.D. thesis, Columbia University (1963)

    work page 1963

  27. [27]

    In: Heller, A

    Lawvere, F.W.: Equality in hyperdoctrines and compreh ension schema as an adjoint functor. In: Heller, A. (ed.) Applications of Categorical Algebra, pp. 1 –14. American Mathematical Society, Providence, R.I. (1970)

    work page 1970

  28. [28]

    Levy, P.B.: Locally graded categories (2019), slides a t https://pblevy.github.io/papers/locgrade.pdf

    work page 2019

  29. [30]

    London Mathematical S ociety Lecture Note Series, Cambridge University Press, Cambridge (2021)

    Loregian, F.: (Co)end Calculus. London Mathematical S ociety Lecture Note Series, Cambridge University Press, Cambridge (2021). https://doi.org/10. 1017/9781108778657

    work page 2021

  30. [31]

    Springer-Verlag New York (1971)

    Mac Lane, S.: Categories for the Working Mathematician . Springer-Verlag New York (1971)

    work page 1971

  31. [32]

    Logica Universalis 7(3), 371–402 (Sep 2013)

    Maietti, M.E., Rosolini, G.: Quotient Completion for t he Foundation of Constructive Mathematics. Logica Universalis 7(3), 371–402 (Sep 2013). https://doi.org/10.1007/s11787 -013-0080-2

    work page doi:10.1007/s11787 2013

  32. [33]

    Applied Categorical Structures 23(1), 24 43–52 (Feb 2015)

    Maietti, M.E., Rosolini, G.: Unifying Exact Completio ns. Applied Categorical Structures 23(1), 24 43–52 (Feb 2015). https://doi.org/10.1007/s10485-013-9 360-5

    work page doi:10.1007/s10485-013-9 2015

  33. [34]

    https://doi.org/https://doi.org/10.1016/j.apal.2022.103234

    Maietti, M.E., Trotta, D.: A characterization of gener alized existential completions 174(4), 103234. https://doi.org/https://doi.org/10.1016/j.apal.2022.103234

    work page doi:10.1016/j.apal.2022.103234 2022

  34. [35]

    In: Proceedings of the 31st Annual ACM/IEEE Symposium on Log ic in Computer Science

    Melli` es, P.A., Zeilberger, N.: A bifibrational recons truction of Lawvere’s presheaf hyperdoctrine. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Log ic in Computer Science. pp. 555–564. LICS ’16, Association for Computing Machinery , New York, NY, USA (Jul 2016). https://doi.org/10.1145/2933575.2934525

    work page doi:10.1145/2933575.2934525 2016

  35. [36]

    The Jour nal of Logic and Algebraic Programming 81(7), 721–781 (2012)

    Meseguer, J.: Twenty years of rewriting logic. The Jour nal of Logic and Algebraic Programming 81(7), 721–781 (2012). https://doi.org/10.1016/j.jlap.20 12.06.003, rewriting Logic and its Appli- cations

    work page doi:10.1016/j.jlap.20 2012

  36. [37]

    In: Kupferman, O., Sobocinski, P

    New, M.S., Licata, D.R.: A Formal Logic for Formal Categ ory Theory. In: Kupferman, O., Sobocinski, P. (eds.) Foundations of Software Science a nd Computation Structures. pp. 113–134. Lecture Notes in Computer Science, Springer Natur e Switzerland, Cham (2023). https://doi.org/10.1007/978-3-031-30829-1 6

    work page doi:10.1007/978-3-031-30829-1 2023

  37. [38]

    E lectronic Notes in Theoretical Com- puter Science 347, 223–239 (Nov 2019)

    North, P.R.: Towards a Directed Homotopy Type Theory. E lectronic Notes in Theoretical Com- puter Science 347, 223–239 (Nov 2019). https://doi.org/10.1016/j.entcs.2 019.09.012

    work page doi:10.1016/j.entcs.2 2019

  38. [39]

    Master’s thesis, KU Leuven (2015)

    Nuyts, A.: Towards a Directed Homotopy Type Theory base d on 4 Kinds of Variance. Master’s thesis, KU Leuven (2015)

    work page 2015

  39. [40]

    Journal of Pu re and Applied Algebra 128(1), 33–92 (Jun 1998)

    Par´ e, R., Rom´ an, L.: Dinatural numbers. Journal of Pu re and Applied Algebra 128(1), 33–92 (Jun 1998). https://doi.org/10.1016/S0022-4049(97)000 36-4

    work page doi:10.1016/s0022-4049(97)000 1998

  40. [41]

    In: Abramsky, S., Gabb ay, D.M., Maibaum, T.S.E

    Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabb ay, D.M., Maibaum, T.S.E. (eds.) Hand- book of Logic in Computer Science: Volume 5: Logic and Algebr aic Methods, pp. 39–123. Oxford University Press (May 1995). https://doi.org/10.1093/os o/9780198537816.003.0002

    work page doi:10.1093/os 1995

  41. [42]

    https://doi.org/10.48550/arXiv.1705.07442

    Riehl, E., Shulman, M.: A type theory for synthetic ∞-categories (May 2017). https://doi.org/10.48550/arXiv.1705.07442

    work page doi:10.48550/arxiv.1705.07442 2017

  42. [43]

    Framed bicategories and monoidal fibrations

    Shulman, M.: Framed bicategories and monoidal fibratio ns. Theory and Applications of Categories 20(18), 650–738 (electronic) (2008). https://doi.org/10.4 8550/arxiv.0706.1286

    work page internal anchor Pith review Pith/arXiv arXiv 2008

  43. [44]

    Shulman, M.: Categorical Logic from a Categorical Poin t of View (2016)

    work page 2016

  44. [45]

    Contravariance through enrichment

    Shulman, M.: Contravariance through enrichment. Theo ry and Applications of Categories 33(5), 95–130 (2018), arXiv:1606.05058

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  45. [46]

    https://homotopytypetheory.org/book, Institute for Advanced Study (2013)

    Univalent Foundations Program, T.: Homotopy Type Theo ry: Univalent Foundations of Mathe- matics. https://homotopytypetheory.org/book, Institute for Advanced Study (2013)

    work page 2013

  46. [47]

    In: Santocanale, L

    Uustalu, T.: A note on strong dinaturality, initial alg ebras and uniform parameterized fixpoint op- erators. In: Santocanale, L. (ed.) 7th Workshop on Fixed Poi nts in Computer Science, FICS 2010, Brno, Czech Republic, August 21-22, 2010. pp. 77–82. Labora toire d’Informatique Fondamentale de Marseille (2010)

    work page 2010

  47. [48]

    equality

    Weaver, M.Z., Licata, D.R.: A Constructive Model of Dir ected Univalence in Bicubical Sets. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Log ic in Computer Science. pp. 915–928. LICS ’20, Association for Computing Machinery , New York, NY, USA (Jul 2020). https://doi.org/10.1145/3373718.3394794 25 A Lawvere on the presheaf hyperdoctrine [...] ...

    work page doi:10.1145/3373718.3394794 2020