20 citations · 30 across the 14 of their papers we have counts for
16 papers
The strength of the minimum principle in constructive reverse mathematics
Tatsuji Kawai
The minimum principle states that every real-valued uniformly continuous function f : X -> R on a compact metric space X attains its minimum. Working in the base system EL0 of cons…
Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma
Tatsuji Kawai
In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point…
Reflexive combinatory algebras
Marlou M. Gijzen, Hajime Ishihara, Tatsuji Kawai
We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which in…
Predicative theories of continuous lattices
Tatsuji Kawai
We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. St…
Decidable fan theorem and uniform continuity theorem with continuous moduli
Makoto Fujiwara, Tatsuji Kawai
The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is s…
Equivalents of the finitary non-deterministic inductive definitions
Ayana Hirata, Hajime Ishihara, Tatsuji Kawai +1
We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of construc…
Representing definable functions of by neighbourhood functions
Tatsuji Kawai
Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's…
Factorizing the Top-Loc adjunction through positive topologies
Francesco Ciraulo, Tatsuji Kawai, Samuele Maschio
We characterize the category of Sambin's positive topologies as a fibration over the category of locales Loc. The fibration is obtained by applying the Grothendieck construction to…
Presenting de Groot duality of stably compact spaces
Tatsuji Kawai
We give a constructive account of the de Groot duality of stably compact spaces in the setting of strong proximity lattice, a point-free representation of a stably compact space. T…
A continuity principle equivalent to the monotone fan theorem
Tatsuji Kawai
The strong continuity principle reads "every pointwise continuous function from a complete separable metric space to a metric space is uniformly continuous near each compact image.…
Principles of bar induction and continuity on Baire space
Tatsuji Kawai
Brouwer-operations, also known as inductively defined neighbourhood functions, provide a good notion of continuity on Baire space which naturally extends that of uniform continuity…
The principle of pointfree continuity
Tatsuji Kawai, Giovanni Sambin
In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuit…
Formally continuous functions on Baire space
Tatsuji Kawai
A function from Baire space to the natural numbers is called formally continuous if it is induced by a morphism between the corresponding formal spaces. We compare formal continuit…
Geometric theories of patch and Lawson topologies
Tatsuji Kawai
We give geometric characterisations of patch and Lawson topologies in the context of predicative point-free topology using the constructive notion of located subset. We present the…
On the commutativity of the powerspace constructions
Matthew de Brecht, Tatsuji Kawai
We investigate powerspace constructions on topological spaces, with a particular focus on the category of quasi-Polish spaces. We show that the upper and lower powerspaces commute…
Localic completion of uniform spaces
Tatsuji Kawai
We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set X…