jespercockx

diff --git a/src/Bool.agda b/src/Bool.agda
index 25a0a7f..ff7c092 100644
--- a/src/Bool.agda
+++ b/src/Bool.agda
@@ -86,7 +86,7 @@ not≡↔≡not {false} {false} =
 
 -- Some lemmas related to T.
 
-T↔≡true : ∀ {b} → T b ↔ b ≡ true
+T↔≡true : {b : Bool} → T b ↔ b ≡ true

jespercockx

{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================

Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.

To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.

This file is a short demo meant to show what you currently can (and can't) do with Prop.

jespercockx

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Size

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

jespercockx

Without covering clauses
-----------------------------------------

512K	./src/Algebra.agdai
28K	./src/Debug/Trace.agdai
72K	./src/Record.agdai
52K	./src/Function.agdai
20K	./src/Strict.agdai
64K	./src/Induction/Lexicographic.agdai
24K	./src/Induction/Nat.agdai

jespercockx

{-# OPTIONS --without-K --rewriting --prop #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A B C : Set ℓ
  x y z : A

jespercockx

How to formalize stuff in Agda
==============================

Preliminaries
-------------

For this presentation, we keep the dependencies to a minimum.

```

jespercockx

How to formalize stuff in Agda

Preliminaries

For this presentation, we keep the dependencies to a minimum.

jespercockx

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Equality

_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
    → (f : {x : A} (y : B x) → C y) (g : (x : A) → B x)
    → (x : A) → C (g x)
(f ∘ g) x = f (g x)

_⁻¹ : {A : Set} {x y : A} → x ≡ y → y ≡ x

jespercockx

open import Agda.Primitive

open import Data.Bool.Base
open import Data.Nat.Base
open import Data.List.Base
open import Data.Product using (_×_; _,_; proj₁; proj₂)
import Data.String.Base as String
open import Data.Unit.Base
open import Function using (id; _∘_)

jespercockx

{-# OPTIONS --rewriting #-}

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Product using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality

Π : (A : Set) (B : A → Set) → Set
Π A B = (x : A) → B x