---
title: "Cubical Type Theoretic Navya-Nyāya"
authors: ["Mrityunjoy Panday", "Sudipta Ghosh"]
year: 2026
venue: "arXiv:cs.LO"
arxiv: "2605.12548"
doi: null
source: "https://arxiv.org/abs/2605.12548"
topics: [curiosity, typed-programming-systems, computational-linguistics-interfaces]
seed_rank: 1455
seed_batch: "curiosity-2026-08-29"
reviewed: "2026-08-29"
pool: "maths-foundations"
relevance_score: 9
lineage: cubical-type-theory
cites:
  - title: "Cubical Type Theory: a constructive interpretation of the univalence axiom"
    url: "https://arxiv.org/abs/1611.02108"
    year: 2016
    arxiv: "1611.02108"
    doi: null
see:
  - "1054-cubical-type-theory"
---

# Cubical Type Theoretic Navya-Nyāya

## One-sentence takeaway

Late-classical Indian Navya-Nyāya logic formalizes cleanly in CCHM cubical type theory — absence, delimitation, and relational depth that FOL/HOL/MLTT each dropped.

## Why it's lovely

Why you might love this: a 17th-century Sanskrit logic school meets De Morgan cubical TT, and the missing pieces (typed absence, non-extensional identity, unbounded relation chains) finally fit.

## Problem

Prior encodings of Navya-Nyāya in FOL (Matilal), HOL (Ganeri), or MLTT (Bhattacharyya) lost avacchedaka, typed abhāva, tādātmya, or paramparā-sambandha.

## Design

- Encode seven core constructs plus qualifier–qualificand structure in CCHM CTT.
- Stratified-universe foundation for the padārtha system.
- Four internal theorems: involution of abhāva, kevalānvayi irreducibility, coextension results, etc.

## Evidence

Constructive formalization claims with named signature theorems inside the encoding.

## Limitations

Philosophy-of-logic formalization, not a drop-in NLP grammar for ano. Completeness vs the historical corpus is partial by design.

## Implications for Broadside

Curiosity sparkle with a linguistics bridge: ano's Japanese/grammar angle likes logics where absence and delimitation are typed, not bolted on.

## Bottom line

Mint the cubical Navya-Nyāya. Old logic, new paths.

## Links

- arXiv abs: https://arxiv.org/abs/2605.12548
- PDF: https://arxiv.org/pdf/2605.12548.pdf