Table of Contents

1 Prelude

2 Function Extensionality

2.3 Implicit Function Extensionality

At times we will need to use a version of function extensionality that works with implicit arguments. We introduce this here.

  implicit-eval :  {i j} {A : Type i} {B : A  Type j}
                   ((x : A)  B x)  {x : A}  B x
  implicit-eval f {x} = f x

implicit-funext :  {i j} {A : Type i} {B : A  Type j} {f g : {x : A}  B x}
                  (H : (x : A)  f {x}  g {x})
                    {x}  f {x})   {x}  g {x})
implicit-funext {f = f} {g = g} H = ap implicit-eval (funextD {f = λ x  f{x}} {g = λ x  g{x}} H)

3 Univalence

4 Propositional resizing

Author: James Leslie

Created: 2021-03-27 Sat 10:47