# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

**20**

votes

**2**answers

2k views

### Prospects for reverse mathematics in Homotopy Type Theory

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include
Subsystems of Second Order Arithmetic (...

**10**

votes

**4**answers

921 views

### Formalizations of the idea that something is a function of something else?

I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...

**14**

votes

**1**answer

2k views

### Forcing in Homotopy Type Theory

I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...

**13**

votes

**2**answers

1k views

### What is the status of (universal) algebra in type theory?

With the recent interest in homotopy type theory as a foundation for mathematics, it seems natural to develop algebra within the framework of type theory. So far, I can't find much literature ...