The following pages link to Ambrus Kaposi (Q2176676):
Displaying 17 items.
- Setoid type theory -- a syntactic translation (Q2176677) (← links)
- Shallow embedding of type theory is morally correct (Q2176685) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- Type theory in type theory using quotient inductive types (Q2828239) (← links)
- Towards a Cubical Type Theory without an Interval (Q4580224) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- Free Applicative Functors (Q4995159) (← links)
- Pointers in Recursion: Exploring the Tropics (Q5089027) (← links)
- Large and Infinitary Quotient Inductive-Inductive Types (Q5145670) (← links)
- (Q5216301) (← links)
- Normalisation by Evaluation for Dependent Types. (Q5369471) (← links)
- (Q5371043) (← links)
- For Finitary Induction-Induction, Induction is Enough (Q6079233) (← links)
- Internal strict propositions using point-free equations (Q6582086) (← links)
- For the metatheory of type theory, internal sconing is enough (Q6622055) (← links)
- Combinatory logic and lambda calculus are equal, algebraically (Q6622066) (← links)
- The Münchhausen method in type theory (Q6643040) (← links)
