Jonas Frey

Search for another author

Author Description

Ask a Question About This Mathematician

All published works (39)

DUALITY FOR CLANS: AN EXTENSION OF GABRIEL–ULMER DUALITY

2025-05-15

Jonas Frey

Abstract Clans are categorical representations of generalized algebraic theories that contain more information than the finite-limit categories associated to the locally finitely presentable categories of models via Gabriel–Ulmer duality. Extending … Abstract Clans are categorical representations of generalized algebraic theories that contain more information than the finite-limit categories associated to the locally finitely presentable categories of models via Gabriel–Ulmer duality. Extending Gabriel–Ulmer duality to account for this additional information, we present a duality theory between clans and locally finitely presentable categories equipped with a weak factorization system of a certain kind.

Zero-Shot Offline Imitation Learning via Optimal Transport

2024-10-11

Thomas Rupf , Marco Bagatella , Nico Gürtler +2 more

Zero-shot imitation learning algorithms hold the promise of reproducing unseen behavior from as little as a single demonstration at test time. Existing practical approaches view the expert demonstration as a … Zero-shot imitation learning algorithms hold the promise of reproducing unseen behavior from as little as a single demonstration at test time. Existing practical approaches view the expert demonstration as a sequence of goals, enabling imitation with a high-level goal selector, and a low-level goal-conditioned policy. However, this framework can suffer from myopic behavior: the agent's immediate actions towards achieving individual goals may undermine long-term objectives. We introduce a novel method that mitigates this issue by directly optimizing the occupancy matching objective that is intrinsic to imitation learning. We propose to lift a goal-conditioned value function to a distance between occupancies, which are in turn approximated via a learned world model. The resulting method can learn from offline, suboptimal data, and is capable of non-myopic, zero-shot imitation, as we demonstrate in complex, continuous benchmarks.

Chat View PDF

Autonomous Forest Inventory with Legged Robots: System Design and Field Deployment

2024-04-22

Matías Mattamala , Nived Chebrolu , Benoît Casseau +5 more

We present a solution for autonomous forest inventory with a legged robotic platform. Compared to their wheeled and aerial counterparts, legged platforms offer an attractive balance of endurance and low … We present a solution for autonomous forest inventory with a legged robotic platform. Compared to their wheeled and aerial counterparts, legged platforms offer an attractive balance of endurance and low soil impact for forest applications. In this paper, we present the complete system architecture of our forest inventory solution which includes state estimation, navigation, mission planning, and real-time tree segmentation and trait estimation. We present preliminary results for three campaigns in forests in Finland and the UK and summarize the main outcomes, lessons, and challenges. Our UK experiment at the Forest of Dean with the ANYmal D legged platform, achieved an autonomous survey of a 0.96 hectare plot in 20 min, identifying over 100 trees with typical DBH accuracy of 2 cm.

Chat View PDF

Uniform Preorders and Partial Combinatory Algebras

2024-03-25

Jonas Frey

Uniform preorders are a class of combinatory representations of Set-indexed preorders that generalize Pieter Hofstra's basic relational objects. An indexed preorder is representable by a uniform preorder if and only … Uniform preorders are a class of combinatory representations of Set-indexed preorders that generalize Pieter Hofstra's basic relational objects. An indexed preorder is representable by a uniform preorder if and only if it has as generic predicate. We study the $\exists$-completion of indexed preorders on the level of uniform preorders, and identify a combinatory condition (called 'relational completeness') which characterizes those uniform preorders with finite meets whose $\exists$-completions are triposes. The class of triposes obtained this way contains relative realizability triposes, for which we derive a characterization as a fibrational analogue of the characterization of realizability toposes given in earlier work. Besides relative partial combinatory algebras, the class of relationally complete uniform preorders contains filtered ordered partial combinatory algebras, and it is unclear if there are any others.

Chat View PDF

RoadRunner - Learning Traversability Estimation for Autonomous Off-road Driving

2024-02-29

Jonas Frey , Shehryar Khattak , Manthan Patel +5 more

Autonomous navigation at high speeds in off-road environments necessitates robots to comprehensively understand their surroundings using onboard sensing only. The extreme conditions posed by the off-road setting can cause degraded … Autonomous navigation at high speeds in off-road environments necessitates robots to comprehensively understand their surroundings using onboard sensing only. The extreme conditions posed by the off-road setting can cause degraded camera image quality due to poor lighting and motion blur, as well as limited sparse geometric information available from LiDAR sensing when driving at high speeds. In this work, we present RoadRunner, a novel framework capable of predicting terrain traversability and an elevation map directly from camera and LiDAR sensor inputs. RoadRunner enables reliable autonomous navigation, by fusing sensory information, handling of uncertainty, and generation of contextually informed predictions about the geometry and traversability of the terrain while operating at low latency. In contrast to existing methods relying on classifying handcrafted semantic classes and using heuristics to predict traversability costs, our method is trained end-to-end in a self-supervised fashion. The RoadRunner network architecture builds upon popular sensor fusion network architectures from the autonomous driving domain, which embed LiDAR and camera information into a common Bird's Eye View perspective. Training is enabled by utilizing an existing traversability estimation stack to generate training data in hindsight in a scalable manner from real-world off-road driving datasets. Furthermore, RoadRunner improves the system latency by a factor of roughly 4, from 500 ms to 140 ms, while improving the accuracy for traversability costs and elevation map predictions. We demonstrate the effectiveness of RoadRunner in enabling safe and reliable off-road navigation at high speeds in multiple real-world driving scenarios through unstructured desert environments.

Chat View PDF

MEM: Multi-Modal Elevation Mapping for Robotics and Learning

2023-10-01

Gian Erni , Jonas Frey , Takahiro Miki +2 more

Elevation maps are commonly used to represent the environment of mobile robots and are instrumental for locomotion and navigation tasks. However, pure geometric information is insufficient for many field applications … Elevation maps are commonly used to represent the environment of mobile robots and are instrumental for locomotion and navigation tasks. However, pure geometric information is insufficient for many field applications that require appearance or semantic information, which limits their applicability to other platforms or domains. In this work, we extend a 2.5D robot-centric elevation mapping framework by fusing multi-modal information from multiple sources into a popular map representation. The framework allows inputting data contained in point clouds or images in a unified manner. To manage the different nature of the data, we also present a set of fusion algorithms that can be selected based on the information type and user requirements. Our system is designed to run on the GPU, making it real-time capable for various robotic and learning tasks. We demonstrate the capabilities of our framework by deploying it on multiple robots with varying sensor configurations and showcasing a range of applications that utilize multi-modal layers, including line detection, human detection, and colorization.

Chat View PDF

Fast Traversability Estimation for Wild Visual Navigation

2023-07-10

Jonas Frey , Matías Mattamala , Nived Chebrolu +3 more

Fig. 1: Wild Visual Navigation (WVN) learns to predict traversability from images via online self-supervised learning.Starting from a randomly initialized traversability estimation network without prior assumptions about the environment (a), … Fig. 1: Wild Visual Navigation (WVN) learns to predict traversability from images via online self-supervised learning.Starting from a randomly initialized traversability estimation network without prior assumptions about the environment (a), a human operator drives the robot around areas that are traversable for the given platform (b).After a few minutes of operation, WVN learns to distinguish between traversable and untraversable areas (c), enabling the robot to navigate autonomously and safely within the environment (d).

Chat View PDF

Constructing coproducts in locally Cartesian closed $\infty$-categories

2023-01-01

Jonas Frey , Nima Rasekh

We prove that every locally Cartesian closed ∞-category with a subobject classifier has a strict initial object and disjoint and universal binary coproducts. We prove that every locally Cartesian closed ∞-category with a subobject classifier has a strict initial object and disjoint and universal binary coproducts.

Chat View PDF

Seeing Through the Grass: Semantic Pointcloud Filter for Support Surface Learning

2023-01-01

Anqiao Li , Chenyu Yang , Jonas Frey +3 more

Mobile ground robots require perceiving and understanding their surrounding support surface to move around autonomously and safely. The support surface is commonly estimated based on exteroceptive depth measurements, e.g., from … Mobile ground robots require perceiving and understanding their surrounding support surface to move around autonomously and safely. The support surface is commonly estimated based on exteroceptive depth measurements, e.g., from LiDARs. However, the measured depth fails to align with the true support surface in the presence of high grass or other penetrable vegetation. In this work, we present the Semantic Pointcloud Filter (SPF), a Convolutional Neural Network (CNN) that learns to adjust LiDAR measurements to align with the underlying support surface. The SPF is trained in a semi-self-supervised manner and takes as an input a LiDAR pointcloud and RGB image. The network predicts a binary segmentation mask that identifies the specific points requiring adjustment, along with estimating their corresponding depth values. To train the segmentation task, 300 distinct images are manually labeled into rigid and non-rigid terrain. The depth estimation task is trained in a self-supervised manner by utilizing the future footholds of the robot to estimate the support surface based on a Gaussian process. Our method can correctly adjust the support surface prior to interacting with the terrain and is extensively tested on the quadruped robot ANYmal. We show the qualitative benefits of SPF in natural environments for elevation mapping and traversability estimation compared to using raw sensor measurements and existing smoothing methods. Quantitative analysis is performed in various natural environments, and an improvement by 48% RMSE is achieved within a meadow terrain.

Chat View PDF

Fast Traversability Estimation for Wild Visual Navigation

2023-01-01

Jonas Frey , Matías Mattamala , Nived Chebrolu +3 more

Natural environments such as forests and grasslands are challenging for robotic navigation because of the false perception of rigid obstacles from high grass, twigs, or bushes. In this work, we … Natural environments such as forests and grasslands are challenging for robotic navigation because of the false perception of rigid obstacles from high grass, twigs, or bushes. In this work, we propose Wild Visual Navigation (WVN), an online self-supervised learning system for traversability estimation which uses only vision. The system is able to continuously adapt from a short human demonstration in the field. It leverages high-dimensional features from self-supervised visual transformer models, with an online scheme for supervision generation that runs in real-time on the robot. We demonstrate the advantages of our approach with experiments and ablation studies in challenging environments in forests, parks, and grasslands. Our system is able to bootstrap the traversable terrain segmentation in less than 5 min of in-field training time, enabling the robot to navigate in complex outdoor terrains - negotiating obstacles in high grass as well as a 1.4 km footpath following. While our experiments were executed with a quadruped robot, ANYmal, the approach presented can generalize to any ground robot.

Chat View PDF

SMUG Planner: A Safe Multi-Goal Planner for Mobile Robots in Challenging Environments

2023-01-01

Changan Chen , Jonas Frey , Philip Arm +1 more

Robotic exploration or monitoring missions require mobile robots to autonomously and safely navigate between multiple target locations in potentially challenging environments. Currently, this type of multi-goal mission often relies on … Robotic exploration or monitoring missions require mobile robots to autonomously and safely navigate between multiple target locations in potentially challenging environments. Currently, this type of multi-goal mission often relies on humans designing a set of actions for the robot to follow in the form of a path or waypoints. In this work, we consider the multi-goal problem of visiting a set of pre-defined targets, each of which could be visited from multiple potential locations. To increase autonomy in these missions, we propose a safe multi-goal (SMUG) planner that generates an optimal motion path to visit those targets. To increase safety and efficiency, we propose a hierarchical state validity checking scheme, which leverages robot-specific traversability learned in simulation. We use LazyPRM* with an informed sampler to accelerate collision-free path generation. Our iterative dynamic programming algorithm enables the planner to generate a path visiting more than ten targets within seconds. Moreover, the proposed hierarchical state validity checking scheme reduces the planning time by 30% compared to pure volumetric collision checking and increases safety by avoiding high-risk regions. We deploy the SMUG planner on the quadruped robot ANYmal and show its capability to guide the robot in multi-goal missions fully autonomously on rough terrain.

Chat View PDF

Duality for Clans: an Extension of Gabriel-Ulmer Duality

2023-01-01

Jonas Frey

Clans are representations of generalized algebraic theories that contain more information than the finite-limit categories associated to the locally finitely presentable categories of models via Gabriel-Ulmer duality. Extending Gabriel-Ulmer duality … Clans are representations of generalized algebraic theories that contain more information than the finite-limit categories associated to the locally finitely presentable categories of models via Gabriel-Ulmer duality. Extending Gabriel-Ulmer duality to account for this additional information, we present a duality theory between clans and locally finitely presentable categories equipped with a weak factorization system of a certain kind.

Chat View PDF

Learning Risk-Aware Quadrupedal Locomotion using Distributional Reinforcement Learning

2023-01-01

Lukas Schneider , Jonas Frey , Takahiro Miki +1 more

Deployment in hazardous environments requires robots to understand the risks associated with their actions and movements to prevent accidents. Despite its importance, these risks are not explicitly modeled by currently … Deployment in hazardous environments requires robots to understand the risks associated with their actions and movements to prevent accidents. Despite its importance, these risks are not explicitly modeled by currently deployed locomotion controllers for legged robots. In this work, we propose a risk sensitive locomotion training method employing distributional reinforcement learning to consider safety explicitly. Instead of relying on a value expectation, we estimate the complete value distribution to account for uncertainty in the robot's interaction with the environment. The value distribution is consumed by a risk metric to extract risk sensitive value estimates. These are integrated into Proximal Policy Optimization (PPO) to derive our method, Distributional Proximal Policy Optimization (DPPO). The risk preference, ranging from risk-averse to risk-seeking, can be controlled by a single parameter, which enables to adjust the robot's behavior dynamically. Importantly, our approach removes the need for additional reward function tuning to achieve risk sensitivity. We show emergent risk sensitive locomotion behavior in simulation and on the quadrupedal robot ANYmal.

Chat View PDF

MEM: Multi-Modal Elevation Mapping for Robotics and Learning

2023-01-01

Gian Erni , Jonas Frey , Takahiro Miki +2 more

Chat View PDF

Resilient Legged Local Navigation: Learning to Traverse with Compromised Perception End-to-End

2023-01-01

Jin Jin , Chong Zhang , Jonas Frey +4 more

Autonomous robots must navigate reliably in unknown environments even under compromised exteroceptive perception, or perception failures. Such failures often occur when harsh environments lead to degraded sensing, or when the … Autonomous robots must navigate reliably in unknown environments even under compromised exteroceptive perception, or perception failures. Such failures often occur when harsh environments lead to degraded sensing, or when the perception algorithm misinterprets the scene due to limited generalization. In this paper, we model perception failures as invisible obstacles and pits, and train a reinforcement learning (RL) based local navigation policy to guide our legged robot. Unlike previous works relying on heuristics and anomaly detection to update navigational information, we train our navigation policy to reconstruct the environment information in the latent space from corrupted perception and react to perception failures end-to-end. To this end, we incorporate both proprioception and exteroception into our policy inputs, thereby enabling the policy to sense collisions on different body parts and pits, prompting corresponding reactions. We validate our approach in simulation and on the real quadruped robot ANYmal running in real-time (<10 ms CPU inference). In a quantitative comparison with existing heuristic-based locally reactive planners, our policy increases the success rate over 30% when facing perception failures. Project Page: https://bit.ly/45NBTuh.

Chat View PDF

Locomotion Policy Guided Traversability Learning using Volumetric Representations of Complex Environments

2022-10-23

Jonas Frey , David Hoeller , Shehryar Khattak +1 more

Despite the progress in legged robotic locomotion, autonomous navigation in unknown environments remains an open problem. Ideally, the navigation system utilizes the full potential of the robots' locomotion capabilities while … Despite the progress in legged robotic locomotion, autonomous navigation in unknown environments remains an open problem. Ideally, the navigation system utilizes the full potential of the robots' locomotion capabilities while operating within safety limits under uncertainty. The robot must sense and analyze the traversability of the surrounding terrain, which depends on the hardware, locomotion control, and terrain properties. It may contain information about the risk, energy, or time consumption needed to traverse the terrain. To avoid hand-crafted traversability cost functions we propose to collect traversability information about the robot and locomotion policy by simulating the traversal over randomly generated terrains using a physics simulator. Thousand of robots are simulated in parallel controlled by the same locomotion policy used in reality to acquire 57 years of real-world locomotion experience equivalent. For deployment on the real robot, a sparse convolutional network is trained to predict the simulated traversability cost, which is tailored to the deployed locomotion policy, from an entirely geometric representation of the environment in the form of a 3D voxel-occupancy map. This representation avoids the need for commonly used elevation maps, which are error-prone in the presence of overhanging obstacles and multi-floor or low-ceiling scenarios. The effectiveness of the proposed traversability prediction network is demonstrated for path planning for the legged robot ANYmal in various indoor and natural environments.

Chat View PDF

Categories of partial equivalence relations as localizations

2022-04-29

Jonas Frey

We construct a category of fibrant objects C〈P〉 in the sense of K. Brown from any indexed frame (a kind of indexed poset generalizing triposes) P, and show that its … We construct a category of fibrant objects C〈P〉 in the sense of K. Brown from any indexed frame (a kind of indexed poset generalizing triposes) P, and show that its homotopy category is the Barr-exact category C[P] of partial equivalence relations and compatible functional relations. In particular this gives a presentation of realizability toposes as homotopy categories. We give criteria for the existence of left and right derived functors to functors C〈Φ〉:C〈P〉→C〈Q〉 induced by finite-meet-preserving transformations Φ:P→Q between indexed frames.

Chat View PDF

Locomotion Policy Guided Traversability Learning using Volumetric Representations of Complex Environments

2022-01-01

Jonas Frey , David Hoeller , Shehryar Khattak +1 more

Chat View PDF

Learning Agile Skills via Adversarial Imitation of Rough Partial Demonstrations

2022-01-01

Chenhao Li , Marin Vlastelica , Sebastian Blaes +3 more

Learning agile skills is one of the main challenges in robotics. To this end, reinforcement learning approaches have achieved impressive results. These methods require explicit task information in terms of … Learning agile skills is one of the main challenges in robotics. To this end, reinforcement learning approaches have achieved impressive results. These methods require explicit task information in terms of a reward function or an expert that can be queried in simulation to provide a target control output, which limits their applicability. In this work, we propose a generative adversarial method for inferring reward functions from partial and potentially physically incompatible demonstrations for successful skill acquirement where reference or expert demonstrations are not easily accessible. Moreover, we show that by using a Wasserstein GAN formulation and transitions from demonstrations with rough and partial information as input, we are able to extract policies that are robust and capable of imitating demonstrated behaviors. Finally, the obtained skills such as a backflip are tested on an agile quadruped robot called Solo 8 and present faithful replication of hand-held human demonstrations.

Chat View PDF

Versatile Skill Control via Self-supervised Adversarial Imitation of Unlabeled Mixed Motions

2022-01-01

Chenhao Li , Sebastian Blaes , Pavel Kolev +3 more

Learning diverse skills is one of the main challenges in robotics. To this end, imitation learning approaches have achieved impressive results. These methods require explicitly labeled datasets or assume consistent … Learning diverse skills is one of the main challenges in robotics. To this end, imitation learning approaches have achieved impressive results. These methods require explicitly labeled datasets or assume consistent skill execution to enable learning and active control of individual behaviors, which limits their applicability. In this work, we propose a cooperative adversarial method for obtaining single versatile policies with controllable skill sets from unlabeled datasets containing diverse state transition patterns by maximizing their discriminability. Moreover, we show that by utilizing unsupervised skill discovery in the generative adversarial imitation learning framework, novel and useful skills emerge with successful task fulfillment. Finally, the obtained versatile policies are tested on an agile quadruped robot called Solo 8 and present faithful replications of diverse skills encoded in the demonstrations.

Chat View PDF

Unsupervised Continual Semantic Adaptation through Neural Rendering

2022-01-01

Zhizheng Liu , Francesco Milano , Jonas Frey +4 more

An increasing amount of applications rely on data-driven models that are deployed for perception tasks across a sequence of scenes. Due to the mismatch between training and deployment data, adapting … An increasing amount of applications rely on data-driven models that are deployed for perception tasks across a sequence of scenes. Due to the mismatch between training and deployment data, adapting the model on the new scenes is often crucial to obtain good performance. In this work, we study continual multi-scene adaptation for the task of semantic segmentation, assuming that no ground-truth labels are available during deployment and that performance on the previous scenes should be maintained. We propose training a Semantic-NeRF network for each scene by fusing the predictions of a segmentation model and then using the view-consistent rendered semantic labels as pseudo-labels to adapt the model. Through joint training with the segmentation model, the Semantic-NeRF model effectively enables 2D-3D knowledge transfer. Furthermore, due to its compact size, it can be stored in a long-term memory and subsequently used to render data from arbitrary viewpoints to reduce forgetting. We evaluate our approach on ScanNet, where we outperform both a voxel-based baseline and a state-of-the-art unsupervised domain adaptation method.

Chat View PDF

Triposes as a generalization of localic geometric morphisms

2021-01-29

Jonas Frey , Thomas Streicher

Abstract In Hyland et al. (1980), Hyland, Johnstone and Pitts introduced the notion of tripos for the purpose of organizing the construction of realizability toposes in a way that generalizes … Abstract In Hyland et al. (1980), Hyland, Johnstone and Pitts introduced the notion of tripos for the purpose of organizing the construction of realizability toposes in a way that generalizes the construction of localic toposes from complete Heyting algebras. In Pitts (2002), one finds a generalization of this notion eliminating an unnecessary assumption of Hyland et al. (1980). The aim of this paper is to characterize triposes over a base topos ${\cal S}$ in terms of so-called constant objects functors from ${\cal S}$ to some elementary topos. Our characterization is slightly different from the one in Pitts’s PhD Thesis (Pitts, 1981) and motivated by the fibered view of geometric morphisms as described in Streicher (2020). In particular, we discuss the question whether triposes over Set giving rise to equivalent toposes are already equivalent as triposes.

Chat View PDF

Constructing Coproducts in locally Cartesian closed $\infty$-Categories

2021-01-01

Jonas Frey , Nima Rasekh

We prove that every locally Cartesian closed $\infty$-category with subobject classifier has a strict initial object and disjoint and universal binary coproducts. We prove that every locally Cartesian closed $\infty$-category with subobject classifier has a strict initial object and disjoint and universal binary coproducts.

Chat View PDF

Continual Adaptation of Semantic Segmentation using Complementary 2D-3D Data Representations

2021-01-01

Jonas Frey , Hermann Blum , Francesco Milano +2 more

Semantic segmentation networks are usually pre-trained once and not updated during deployment. As a consequence, misclassifications commonly occur if the distribution of the training data deviates from the one encountered … Semantic segmentation networks are usually pre-trained once and not updated during deployment. As a consequence, misclassifications commonly occur if the distribution of the training data deviates from the one encountered during the robot's operation. We propose to mitigate this problem by adapting the neural network to the robot's environment during deployment, without any need for external supervision. Leveraging complementary data representations, we generate a supervision signal, by probabilistically accumulating consecutive 2D semantic predictions in a volumetric 3D map. We then train the network on renderings of the accumulated semantic map, effectively resolving ambiguities and enforcing multi-view consistency through the 3D representation. In contrast to scene adaptation methods, we aim to retain the previously-learned knowledge, and therefore employ a continual learning experience replay strategy to adapt the network. Through extensive experimental evaluation, we show successful adaptation to real-world indoor scenes both on the ScanNet dataset and on in-house data recorded with an RGB-D sensor. Our method increases the segmentation accuracy on average by 9.9% compared to the fixed pre-trained neural network, while retaining knowledge from the pre-training dataset.

Chat View PDF

Triposes as a Generalization of Localic Geometric Morphisms

2020-01-01

Jonas Frey , Thomas Streicher

We discuss how triposes may be understood as generalizations of localic geometric morphisms. We discuss how triposes may be understood as generalizations of localic geometric morphisms.

Chat View PDF

Categories of partial equivalence relations as localizations

2019-01-01

Jonas Frey

We construct a category of fibrant objects $\mathbb{C}\langle P\rangle$ in the sense of K. Brown from any indexed frame (a kind of indexed poset generalizing triposes) $P$, and show that … We construct a category of fibrant objects $\mathbb{C}\langle P\rangle$ in the sense of K. Brown from any indexed frame (a kind of indexed poset generalizing triposes) $P$, and show that its homotopy category is the Barr-exact category $\mathbb{C}[P]$ of partial equivalence relations and compatible functional relations. In particular this gives a presentation of realizability toposes as homotopy categories. We give criteria for the existence of left and right derived functors to functors $\mathbb{C}\langle\Phi\rangle : \mathbb{C}\langle P\rangle\to \mathbb{C}\langle Q\rangle$ induced by finite-meet-preserving transformations ${\Phi} : P \to Q$ between indexed frames.

Chat View PDF

Characterizing partitioned assemblies and realizability toposes

2018-08-22

Jonas Frey

Chat View PDF

Impredicative Encodings of (Higher) Inductive Types

2018-06-27

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

Chat View PDF

Impredicative Encodings of (Higher) Inductive Types

2018-01-01

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

Chat View PDF

Ordered combinatory algebras and realizability

2015-09-10

Walter Ferrer Santos , Jonas Frey , Mauricio Guillermo +2 more

We propose the new concept of Krivine ordered combinatory algebra ( $\mathcal{^KOCA}$ ) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show … We propose the new concept of Krivine ordered combinatory algebra ( $\mathcal{^KOCA}$ ) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that $\mathcal{^KOCA}$ 's are equivalent to Streicher's abstract Krivine structures for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of triposes . The difference between the two representations is that the elements of a $\mathcal{^KOCA}$ play both the role of truth values and realizers, whereas truth values are sets of realizers in $\mathcal{AKS}$ s. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a $\mathcal{^KOCA}$ , which showcases the dual role that is played by the elements of the $\mathcal{^KOCA}$ .

Chat View PDF

Realizability Toposes from Specifications

2015-01-01

Jonas Frey

We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations … We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of `pole' and `proof-like term'. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.

Chat View PDF

Triposes, q-toposes and toposes

2014-11-20

Jonas Frey

Ordered combinatory algebras and realizability

2014-10-19

Walter Ferrer Santos , Jonas Frey , Mauricio Guillermo +2 more

We consider different classes of combinatory structures related to realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are equivalent … We consider different classes of combinatory structures related to realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are equivalent for the purpose of modeling higher-order logic. We center our attentions in the role of a special kind of Ordered Combinatory Algebras-- that we call the Krivine ordered combinatory algebras ($\mathcal{KOCA}$s)-- that we propose as the foundational pillars for the categorical perspective of Krivine's classical realizability as presented by Streicher. Our procedure is the following: we show that each of the considered combinatory structures gives rise to an indexed preorder, and describe a way to transform the different structures into each other that preserves the associated indexed preorders up to equivalence. Since all structures give rise to the same indexed preorders, we only prove that they are triposes once: for the class of $\mathcal{KOCA}$s. We finish showing that in $\mathcal{KOCA}$s, one can define realizability in every higher-order language and in particular in higher-order arithmetic.

Chat View PDF

A Characterization of Realizability Toposes

2014-04-28

Jonas Frey

Chat View PDF

Characterizing partitioned assemblies and realizability toposes

2014-04-28

Jonas Frey

We give simple characterizations of the category PAsm(A) of partitioned assemblies, and of the realizability topos RT(A) over a partial combinatory algebra A. This answers the question for an 'extensional … We give simple characterizations of the category PAsm(A) of partitioned assemblies, and of the realizability topos RT(A) over a partial combinatory algebra A. This answers the question for an 'extensional characterization' of realizability toposes.

Chat View PDF

A fibrational study of realizability toposes

2014-01-01

Jonas Frey

This is the author's PhD thesis. It is a contribution to categorical logic, in particular to the theory of realizability toposes. While the tools of categorical logic have proven very … This is the author's PhD thesis. It is a contribution to categorical logic, in particular to the theory of realizability toposes. While the tools of categorical logic have proven very successful in analyzing and organizing proof theoretic realizability interpretations, it was remarked by experts (notably Peter Johnstone) that the field of realizability toposes itself was not clearly delineated, and lacked a powerful theory analogous to that of Grothendieck toposes. The present work sets out to remedy this situation to a certain extent. We argue that realizability toposes are best understood using Grothendieck fibrations, and develop a framework of fibrational cocompletions, which allows to view certain constructions from realizability in precise analogy to constructions of presheaf and sheaf toposes. Using these techniques, and a class of posetal fibrations that we call uniform preorders, we are able to give an extensional characterization of partial combinatory algebras and of the realizability toposes that are constructed from these algebras. Striving to develop the analogy to Grothendieck toposes further, we outline how to apply our techniques on arbitrary base toposes, and give a decomposition theorem for constant objects functors induced by triposes, analogous to the known decompositions of geometric morphisms. Finally, we sketch an approach of how to find a unified framework for Grothendieck toposes and realizability toposes, based on the observation that uniform preorders can be identified with preorders internal to a category of sheaves.

Chat View PDF

Ordered combinatory algebras and realizability

2014-01-01

Walter Ferrer Santos , Jonas Frey , Mauricio Guillermo +2 more

We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are … We consider different classes of combinatory structures related to Krivine realizability. We show, in the precise sense that they give rise to the same class of triposes, that they are equivalent for the purpose of modeling higher-order logic. We center our attentions in the role of a special kind of Ordered Combinatory Algebras-- that we call the "Krivine ordered combinatory algebras" ($\mathcal{KOCA}$s)-- that we propose as the foundational pillars for the categorical perspective of Krivine's classical realizability as presented by Streicher. Our procedure is the following: we show that each of the considered combinatory structures gives rise to an indexed preorder, and describe a way to transform the different structures into each other that preserves the associated indexed preorders up to equivalence. Since all structures give rise to the same indexed preorders, we only prove that they are triposes once: for the class of $\mathcal{KOCA}$s. We finish showing that in $\mathcal{KOCA}$s, one can define realizability in every higher-order language and in particular in higher-order arithmetic.

Chat View PDF

Characterizing partitioned assemblies and realizability toposes

2014-01-01

Jonas Frey

Chat View PDF

A 2-Categorical Analysis of the Tripos-to-Topos Construction

2011-01-01

Jonas Frey

We characterize the tripos-to-topos construction of Hyland, Johnstone and Pitts as a biadjunction in a bicategory enriched category of equipment-like structures. These abstract concepts are necessary to handle the presence … We characterize the tripos-to-topos construction of Hyland, Johnstone and Pitts as a biadjunction in a bicategory enriched category of equipment-like structures. These abstract concepts are necessary to handle the presence of oplax constructs --- the construction is only oplax functorial on certain classes of cartesian functors between triposes. A by-product of our analysis is the decomposition of the tripos-to-topos construction into two steps, the intermediate step being a weakened version of quasitoposes.

Chat View PDF

Common Coauthors

Coauthor	Papers Together
Marco Hutter	13
Matías Mattamala	6
César Cadena	6
Shehryar Khattak	3
Nived Chebrolu	3
Octavio Malherbe	3
Maurice Fallon	3
Georg Martius	3
Mauricio Guillermo	3
Walter Ferrer Santos	3
Alexandre Miquel	3
Takahiro Miki	2
Marin Vlastelica	2
Gian Erni	2
Nima Rasekh	2
Hermann Blum	2
David Hoeller	2
Francesco Milano	2
Steve Awodey	2
Sam Speight	2
Roland Siegwart	2
Thomas Streicher	2
Sebastian Blaes	2
Manthan Patel	1
Anqiao Li	1
Pavel Kolev	1
Thomas Rupf	1
Curtis Padgett	1
Patrick Spieler	1
Julian Nubert	1
Zhizheng Liu	1
Nico Gürtler	1
Lukas Schneider	1
Nikita Rudin	1
Deegan Atha	1
Benoît Casseau	1
Philip Arm	1
Takahiro Miki	1
Changan Chen	1
Marco Bagatella	1
Leonard Freißmuth	1
Felix Grimminger	1
Chenhao Li	1
Turcan Tuna	1
Chong Zhang	1
Jin Jin	1
Joonho Lee	1
Chenyu Yang	1
Chenhao Li	1

Commonly Cited References

Tripos theory in retrospect

2002-06-01

Andrew M. Pitts

The notion of tripos (Hyland et al. 1980; Pitts 1981) was motivated by the desire to explain in what sense Higg's description of sheaf toposes as H-valued sets and Hyland's … The notion of tripos (Hyland et al. 1980; Pitts 1981) was motivated by the desire to explain in what sense Higg's description of sheaf toposes as H-valued sets and Hyland's realizability toposes are instances of the same construction. The construction itself can be seen as the universal solution to the problem of realizing the predicates of a first order hyperdoctrine as subobjects in a logos with effective equivalence relations. In this note it is shown that the resulting logos is actually a topos if and only if the original hyperdoctrine satisfies a certain comprehension property. Triposes satisfy this property, but there are examples of non-triposes satisfying this form of comprehension.

Realizability Categories

2013-01-01

Wouter Pieter Stekelenburg

This is the author's Ph.D. Thesis. It contains results from four years of research into realizability and categorical logic. The main subjects are the axiomatisation of realizable propositions, and a … This is the author's Ph.D. Thesis. It contains results from four years of research into realizability and categorical logic. The main subjects are the axiomatisation of realizable propositions, and a characterization of realizability categories as pseudoinitial objects. Realizability is a collection of techniques in the study of constructive logic. Some forms of realizability induce realizability categories, which are Heyting categories and therefore have a first order intuitionistic logic as internal language. The axiomatisation chapter of the thesis explains how and to what extend we can axiomatise the set of valid propositions in this internal language. The realizability categories chapter explains how to find regular functors from realizability categories into other categories.

Chat View PDF

Tripos theory

1980-09-01

J. M. E. Hyland , Peter Johnstone , Andrew M. Pitts

One of the most important constructions in topos theory ia that of the category Shv ( A ) of sheaves on a locale (= complete Heyting algebra) A. Normally, the … One of the most important constructions in topos theory ia that of the category Shv ( A ) of sheaves on a locale (= complete Heyting algebra) A. Normally, the objects of this category are described as ‘presheaves on A satisfying a gluing condition’; but, as Higgs(7) and Fourman and Scott(5) have observed, they may also be regarded as ‘sets structured with an A -valued equality predicate’ (briefly, ‘ A -valued sets’). From the latter point of view, it is an inessential feature of the situation that every sheaf has a canonical representation as a ‘complete’ A -valued set. In this paper, our aim is to investigate those properties which A must have for us to be able to construct a topos of A -valued sets: we shall see that there is one important respect, concerning the relationship between the finitary (propositional) structure and the infinitary (quantifier) structure, in which the usual definition of a locale may be relaxed, and we shall give a number of examples (some of which will be explored more fully in a later paper (8)) to show that this relaxation is potentially useful.

Categories for the Working Mathematician

1971-01-01

Saunders Mac Lane

Chat View PDF

A fibrational study of realizability toposes

2014-01-01

Jonas Frey

Chat View PDF

Elevation Mapping for Locomotion and Navigation using GPU

2022-10-23

Takahiro Miki , Lorenz Wellhausen , Ruben Grandia +3 more

Perceiving the surrounding environment is crucial for autonomous mobile robots. An elevation map provides a memory-efficient and simple yet powerful geometric represen-tation of the terrain for ground robots. The robots … Perceiving the surrounding environment is crucial for autonomous mobile robots. An elevation map provides a memory-efficient and simple yet powerful geometric represen-tation of the terrain for ground robots. The robots can use this information for navigation in an unknown environment or perceptive locomotion control over rough terrain. Depending on the application, various post processing steps may be incorpo-rated, such as smoothing, inpainting or plane segmentation. In this work, we present an elevation mapping pipeline leveraging GPU for fast and efficient processing with additional features both for navigation and locomotion. We demonstrated our map-ping framework through extensive hardware experiments. Our mapping software was successfully deployed for underground exploration during DARPA Subterranean Challenge and for various experiments of quadrupedal locomotion.

Chat View PDF

Iterated realizability as a comma construction

2008-01-01

Pieter Hofstra

Abstract We show that the 2-category of partial combinatory algebras, as well as various related categories, admit a certain type of lax comma objects. This not only reveals some of … Abstract We show that the 2-category of partial combinatory algebras, as well as various related categories, admit a certain type of lax comma objects. This not only reveals some of the properties of such categories, but it also gives an interpretation of iterated realizability, in the following sense. Let φ: A → B be a morphism of PCAs, giving a comma object A ⋉ φ B . In the realizability topos RT ( B ) over B , the object ( A , φ) is an internal PCA, so we can construct the realizability topos over ( A , φ). This topos is equivalent to the realizability topos over the comma-PCA A ⋉ φ B . This result is both an analysis and a generalization of a special case studied by Pitts in the context of the effective monad.

Chat View PDF

A characterization of the left exact categories whose exact completions are toposes

2003-01-21

Matı́as Menni

Locally cartesian closed exact completions

2000-12-01

A. Carboni , Giuseppe Rosolini

A 2-Categories Companion

2009-09-16

Stephen Lack

This paper is a rather informal guide to some of the basic theory of 2-categories and bicategories, including notions of limit and colimit, 2-dimensional universal algebra, formal category theory, and … This paper is a rather informal guide to some of the basic theory of 2-categories and bicategories, including notions of limit and colimit, 2-dimensional universal algebra, formal category theory, and nerves of bicategories. As is the way of these things, the choice of topics is somewhat personal. No attempt is made at either rigour or completeness. Nor is it completely introductory: you will not find a definition of bicategory; but then nor will you really need one to read it. In keeping with the philosophy of category theory, the morphisms between bicategories play more of a role than the bicategories themselves.

Chat View PDF

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these … Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.

Chat View PDF

La logique des topos

1981-03-01

André Boileau , André Joyal

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie … Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie algébrique sous la forme élaborée par Grothendieck. (2) La logique formelle. Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes: (1) Mathématique intuitionniste. (2) Forcing de Cohen et Robinson. (3) Logique algébrique. (4) Géométrie algébrique. (5) Géométrie différentielle et analytique. (6) Topologie algébrique: cohomologie, homotopie. (7) Théorie de Galois. Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3). La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8]. Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

Inductive Types in Homotopy Type Theory

2012-06-01

Steve Awodey , Nicola Gambino , Kristina Sojakova

Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional … Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

Chat View PDF

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition … We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

Chat View PDF

A small complete category

1988-11-01

J. M. E. Hyland

Implicative algebras: a new foundation for realizability and forcing

2020-05-01

Alexandre Miquel

We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature … We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (Set-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompass all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine) and all intuitionistic realizability triposes built from partial combinatory algebras.

Chat View PDF

Categories of continuous functors, I

1972-09-01

Peter Freyd , G. M. Kelly

Emerging Properties in Self-Supervised Vision Transformers

2021-10-01

Mathilde Caron , Hugo Touvron , Ishan Misra +4 more

In this paper, we question if self-supervised learning provides new properties to Vision Transformer (ViT) [16] that stand out compared to convolutional networks (convnets). Beyond the fact that adapting self-supervised … In this paper, we question if self-supervised learning provides new properties to Vision Transformer (ViT) [16] that stand out compared to convolutional networks (convnets). Beyond the fact that adapting self-supervised methods to this architecture works particularly well, we make the following observations: first, self-supervised ViT features contain explicit information about the semantic segmentation of an image, which does not emerge as clearly with supervised ViTs, nor with convnets. Second, these features are also excellent k-NN classifiers, reaching 78.3% top-1 on ImageNet with a small ViT. Our study also underlines the importance of momentum encoder [26], multi-crop training [9], and the use of small patches with ViTs. We implement our findings into a simple self-supervised method, called DINO, which we interpret as a form of self-distillation with no labels. We show the synergy between DINO and ViTs by achieving 80.1% top-1 on ImageNet in linear evaluation with ViT-Base.

Chat View PDF

Learning Ground Traversability From Simulations

2018-02-05

R. Omar Chavéz-García , Jérôme Guzzi , Luca Maria Gambardella +1 more

Mobile ground robots operating on unstructured terrain must predict which areas of the environment they are able to pass in order to plan feasible paths. We address traversability estimation as … Mobile ground robots operating on unstructured terrain must predict which areas of the environment they are able to pass in order to plan feasible paths. We address traversability estimation as a heightmap classification problem: we build a convolutional neural network that, given an image representing the heightmap of a terrain patch, predicts whether the robot will be able to traverse such patch from left to right. The classifier is trained for a specific robot model (wheeled, tracked, legged, snake-like) using simulation data on procedurally generated training terrains; the trained classifier can be applied to unseen large heightmaps to yield oriented traversability maps, and then plan traversable paths. We extensively evaluate the approach in simulation on six real-world elevation datasets, and run a real-robot validation in one indoor and one outdoor environment.

Chat View PDF

Learning robust perceptive locomotion for quadrupedal robots in the wild

2022-01-19

Takahiro Miki , Joonho Lee , Jemin Hwangbo +3 more

Legged robots that can operate autonomously in remote and hazardous environments will greatly increase opportunities for exploration into under-explored areas. Exteroceptive perception is crucial for fast and energy-efficient locomotion: perceiving … Legged robots that can operate autonomously in remote and hazardous environments will greatly increase opportunities for exploration into under-explored areas. Exteroceptive perception is crucial for fast and energy-efficient locomotion: perceiving the terrain before making contact with it enables planning and adaptation of the gait ahead of time to maintain speed and stability. However, utilizing exteroceptive perception robustly for locomotion has remained a grand challenge in robotics. Snow, vegetation, and water visually appear as obstacles on which the robot cannot step~-- or are missing altogether due to high reflectance. Additionally, depth perception can degrade due to difficult lighting, dust, fog, reflective or transparent surfaces, sensor occlusion, and more. For this reason, the most robust and general solutions to legged locomotion to date rely solely on proprioception. This severely limits locomotion speed, because the robot has to physically feel out the terrain before adapting its gait accordingly. Here we present a robust and general solution to integrating exteroceptive and proprioceptive perception for legged locomotion. We leverage an attention-based recurrent encoder that integrates proprioceptive and exteroceptive input. The encoder is trained end-to-end and learns to seamlessly combine the different perception modalities without resorting to heuristics. The result is a legged locomotion controller with high robustness and speed. The controller was tested in a variety of challenging natural and urban environments over multiple seasons and completed an hour-long hike in the Alps in the time recommended for human hikers.

Chat View PDF

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

Chat View PDF

Locomotion Policy Guided Traversability Learning using Volumetric Representations of Complex Environments

2022-10-23

Jonas Frey , David Hoeller , Shehryar Khattak +1 more

Chat View PDF

Homotopy-Initial Algebras in Type Theory

2017-01-30

Steve Awodey , Nicola Gambino , Kristina Sojakova

We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a … We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.

Chat View PDF

Framed bicategories and monoidal fibrations

2007-01-01

Michael Shulman

In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or … In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical fibrations. The resulting `framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a `monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Chat View PDF

Towards a theory of type structure

1974-01-01

John Reynolds

Chat View PDF

Higher Topos Theory (AM-170)

2009-12-31

Jacob Lurie

Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are … Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are assumed to be invertible. In Higher Topos Theory , Jacob Lurie presents the foundations of this theory, using the language of weak Kan complexes introduced by Boardman and Vogt, and shows how existing theorems in algebraic topology can be reformulated and generalized in the theory's new language. The result is a powerful theory with applications in many areas of mathematics. The book's first five chapters give an exposition of the theory of infinity-categories that emphasizes their role as a generalization of ordinary categories. Many of the fundamental ideas from classical category theory are generalized to the infinity-categorical setting, such as limits and colimits, adjoint functors, ind-objects and pro-objects, locally accessible and presentable categories, Grothendieck fibrations, presheaves, and Yoneda's lemma. A sixth chapter presents an infinity-categorical version of the theory of Grothendieck topoi, introducing the notion of an infinity-topos, an infinity-category that resembles the infinity-category of topological spaces in the sense that it satisfies certain axioms that codify some of the basic principles of algebraic topology. A seventh and final chapter presents applications that illustrate connections between the theory of higher topoi and ideas from classical topology.

Voxblox: Incremental 3D Euclidean Signed Distance Fields for on-board MAV planning

2017-09-01

Helen Oleynikova , Zachary Taylor , Marius Fehr +2 more

Micro Aerial Vehicles (MAVs) that operate in unstructured, unexplored environments require fast and flexible local planning, which can replan when new parts of the map are explored. Trajectory optimization methods … Micro Aerial Vehicles (MAVs) that operate in unstructured, unexplored environments require fast and flexible local planning, which can replan when new parts of the map are explored. Trajectory optimization methods fulfill these needs, but require obstacle distance information, which can be given by Euclidean Signed Distance Fields (ESDFs). We propose a method to incrementally build ESDFs from Truncated Signed Distance Fields (TSDFs), a common implicit surface representation used in computer graphics and vision. TSDFs are fast to build and smooth out sensor noise over many observations, and are designed to produce surface meshes. We show that we can build TSDFs faster than Octomaps, and that it is more accurate to build ESDFs out of TSDFs than occupancy maps. Our complete system, called voxblox, is available as open source and runs in real-time on a single CPU core. We validate our approach on-board an MAV, by using our system with a trajectory optimization local planner, entirely on-board and in real-time.

Chat View PDF

Regular and exact completions

1998-03-01

A. Carboni , E. M. Vitale

Wellfounded Trees and Dependent Polynomial Functors

2004-01-01

Nicola Gambino , Martin Hyland

Chat View PDF

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-01

Daniel R. Licata , Michael Shulman

Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new … Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.

Chat View PDF

Type theories, toposes and constructive set theory: predicative aspects of AST

2002-04-01

Ieke Moerdijk , Erik Palmgren

Chat View PDF

The free exact category on a left exact one

1982-12-01

A. Carboni , R. Celia Magno

Abstract We give an explicit one step description of the free (Barr) exact category on a left exact one. As an application we give a new two step construction of … Abstract We give an explicit one step description of the free (Barr) exact category on a left exact one. As an application we give a new two step construction of the free abelian category on an additive one.

Chat View PDF

Unifying Exact Completions

2013-12-04

Maria Emilia Maietti , Giuseppe Rosolini

Chat View PDF

Basic Bicategories

1998-10-04

Tom Leinster

A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem. A concise guide to very basic bicategory theory, from the definition of a bicategory to the coherence theorem.

Chat View PDF

On the sphere of origin of infinite families in the homotopy groups of spheres

1969-07-01

Brayton Gray

Strong functors and monoidal monads

1972-12-01

Anders Kock

Abstract homotopy theory and generalized sheaf cohomology

1973-01-01

Kenneth S. Brown

Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kanâs category of spectra. These groups generalize the ordinary … Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kanâs category of spectra. These groups generalize the ordinary cohomology groups of X with coefficients in an abelian sheaf, as well as the generalized cohomology of X in the usual sense. The groups are defined by means of the âhomotopical algebraâ of Quillen applied to suitable categories of sheaves. The study of the homotopy category of sheaves of spectra requires an abstract homotopy theory more general than Quillenâs, and this is developed in Part I of the paper. Finally, the basic cohomological properties are proved, including a spectral sequence which generalizes the Atiyah-Hirzebruch spectral sequence (in generalized cohomology theory) and the âlocal to globalâ spectral sequence (in sheaf cohomology theory).

Chat View PDF

On a fat small object argument

2014-01-11

Michael Makkai , Jir̆ı́ Rosický , Lukáš Vokřínek

Good colimits introduced by J. Lurie generalize transfinite composites and provide an important tool for understanding cofibrant generation in locally presentable categories. We will explore the relation of good colimits … Good colimits introduced by J. Lurie generalize transfinite composites and provide an important tool for understanding cofibrant generation in locally presentable categories. We will explore the relation of good colimits to transfinite composites further and show, in particular, how they eliminate the use of large objects in the usual small object argument.

Chat View PDF

A Survey of (∞, 1)-Categories

2009-09-16

Julia E. Bergner

In this paper we give a summary of the comparisons between different definitions of so-called (∞, 1)-categories, which are considered to be models for ∞-categories whose n-morphisms are all invertible … In this paper we give a summary of the comparisons between different definitions of so-called (∞, 1)-categories, which are considered to be models for ∞-categories whose n-morphisms are all invertible for n > 1. They are also, from the viewpoint of homotopy theory, models for the homotopy theory of homotopy theories. The four different structures, all of which are equivalent, are simplicial categories, Segal categories, complete Segal spaces, and quasi-categories.

Introduction to bicategories

1967-01-01

Jean Bénabou

Enhanced 2-categories and limits for lax morphisms

2011-10-03

Stephen Lack , Michael Shulman

Chat View PDF

Introduction to extensive and distributive categories

1993-02-01

A. Carboni , Stephen Lack , R. F. C. Walters

Semi-abelian categories

2002-03-01

George Janelidze , L. Márki , Walter Tholen

Exact completions and small sheaves

2012-01-01

Michael Shulman

We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal … We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal k. A k-ary exact category is an exact category with disjoint and universal k-small coproducts, and a k-ary site is a site whose covering sieves are generated by k-small families and which satisfies a weak size condition. For different values of k, this includes the exact completions of a regular category or a category with (weak) finite limits; the pretopos completion of a coherent category; and the category of sheaves on a small site. For a large site with k the size of the universe, it gives a well-behaved "category of small sheaves". Along the way, we define a slightly generalized notion of "morphism of sites", and show that k-ary sites are equivalent to a type of "enhanced allegory".

Chat View PDF

Lattice theoretic and logical aspects of elementary topoi

1976-01-01

Christian Juul Mikkelsen

Simplicial Homotopy Theory

2009-01-01

Paul G. Goerss , John F. Jardine

Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c

Chat View PDF

Fibered categories and the foundations of naive category theory

1985-03-01

Jean Bénabou

Any attempt to give “foundations”, for category theory or any domain in mathematics, could have two objectives, of course related. (0.1) Noncontradiction : Namely, to provide a formal frame rich … Any attempt to give “foundations”, for category theory or any domain in mathematics, could have two objectives, of course related. (0.1) Noncontradiction : Namely, to provide a formal frame rich enough so that all the actual activity in the domain can be carried out within this frame, and consistent, or at least relatively consistent with a well-established and “safe” theory, e.g. Zermelo-Frankel (ZF). (0.2) Adequacy , in the following, nontechnical sense: (i) The basic notions must be simple enough to make transparent the syntactic structures involved. (ii) The translation between the formal language and the usual language must be, or very quickly become, obvious. This implies in particular that the terminology and notations in the formal system should be identical, or very similar, to the current ones. Although this may seem minor, it is in fact very important. (iii) “Foundations” can only be “foundations of a given domain at a given moment”, therefore the frame should be easily adaptable to extensions or generalizations of the domain, and, even better, in view of (i), it should suggest how to find meaningful generalizations. (iv) Sometimes (ii) and (iii) can be incompatible because the current notations are not adapted to a more general situation. A compromise is then necessary. Usually when the tradition is very strong (ii) is predominant, but this causes some incoherence for the notations in the more general case (e.g. the notation f ( x ) for the value of a function f at x obliges one, in category theory, to denote the composition of arrows ( f, g ) → g∘f , and all attempts to change this notation have, so far, failed).

Elementary observations on 2-categorical limits

1989-04-01

G. M. Kelly

With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be … With a view to further applications, we give a self-contained account of indexed limits for 2-categories, including necessary and sufficient conditions for 2-categorical completeness. Many important 2-categories fail to be complete but do admit a wide class of limits. Accordingly, we introduce a variety of particular 2-categorical limits of practical importance, and show that certain of these suffice for the existence of indexed lax- and pseudo-limits. Other important 2-categories fail to admit even pseudo-limits, but do admit the weaker bilimits; we end by discussing these.

Chat View PDF

A notion of homotopy for the effective topos

2014-11-17

Jaap van Oosten

We define a notion of homotopy in the effective topos. We define a notion of homotopy in the effective topos.

Chat View PDF

Some free constructions in realizability and proof theory

1995-09-01

A. Carboni