{-# OPTIONS --without-K #-} module EqualityBase where open import Universes public variable 𝓣 𝓀 π“₯ 𝓦 : Universe {- Defining the unary type -} data πŸ™ : 𝓀₀ Μ‡ where * : πŸ™ πŸ™-induction : (A : πŸ™ β†’ π“€β€ŠΜ‡ ) β†’ A * β†’ (x : πŸ™) β†’ A x πŸ™-induction A a * = a πŸ™-recursion : (B : π“€β€ŠΜ‡ ) β†’ B β†’ (πŸ™ β†’ B) πŸ™-recursion B b x = πŸ™-induction (Ξ» _ β†’ B) b x !πŸ™' : (X : π“€β€ŠΜ‡ ) β†’ X β†’ πŸ™ !πŸ™' X x = * !πŸ™ : {X : π“€β€ŠΜ‡ } β†’ X β†’ πŸ™ !πŸ™ x = * {- Defining the nullary type -} data 𝟘 : π“€β‚€β€ŠΜ‡ where 𝟘-induction : (A : 𝟘 β†’ 𝓀 Μ‡ ) β†’ (x : 𝟘) β†’ A x 𝟘-induction A () 𝟘-recursion : (A : 𝓀 Μ‡ ) β†’ 𝟘 β†’ A 𝟘-recursion A a = 𝟘-induction (Ξ» _ β†’ A) a !𝟘 : (A : 𝓀 Μ‡ ) β†’ 𝟘 β†’ A !𝟘 = 𝟘-recursion is-empty : 𝓀 Μ‡ β†’ 𝓀 Μ‡ is-empty X = X β†’ 𝟘 Β¬ : 𝓀 Μ‡ β†’ 𝓀 Μ‡ Β¬ X = X β†’ 𝟘 {- Definition of the natural numbers -} data β„• : 𝓀₀ Μ‡ where zero : β„• succ : β„• β†’ β„• {-# BUILTIN NATURAL β„• #-} β„•-induction : (A : β„• β†’ 𝓀 Μ‡ ) β†’ A 0 β†’ ((n : β„•) β†’ A n β†’ A (succ n)) β†’ (n : β„•) β†’ A n β„•-induction A aβ‚€ f = h where h : (n : β„•) β†’ A n h 0 = aβ‚€ h (succ n) = f n (h n) β„•-recursion : (X : 𝓀 Μ‡ ) β†’ X β†’ (β„• β†’ X β†’ X) β†’ β„• β†’ X β„•-recursion X = β„•-induction (Ξ» _ β†’ X) β„•-iteration : (X : 𝓀 Μ‡ ) β†’ X β†’ (X β†’ X) β†’ β„• β†’ X β„•-iteration X x f = β„•-recursion X x (Ξ» _ x β†’ f x) module Arithmetic where _+_ _Γ—_ : β„• β†’ β„• β†’ β„• x + 0 = x x + succ y = succ (x + y) x Γ— 0 = 0 x Γ— succ y = x + x Γ— y infixl 20 _+_ infixl 21 _Γ—_ module β„•-order where _≀_ _β‰₯_ : β„• β†’ β„• β†’ 𝓀₀ Μ‡ 0 ≀ y = πŸ™ succ x ≀ 0 = 𝟘 succ x ≀ succ y = x ≀ y x β‰₯ y = y ≀ x infix 10 _≀_ infix 10 _β‰₯_ {- Definition of the sum type -} data _+_ {𝓀 π“₯} (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ ) : 𝓀 βŠ” π“₯ Μ‡ where inl : X β†’ X + Y inr : Y β†’ X + Y +-induction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X + Y β†’ 𝓦 Μ‡ ) β†’ ((x : X) β†’ A (inl x)) β†’ ((y : Y) β†’ A (inr y)) β†’ (z : X + Y) β†’ A z +-induction A f g (inl x) = f x +-induction A f g (inr y) = g y +-recursion : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } β†’ (X β†’ A) β†’ (Y β†’ A) β†’ X + Y β†’ A +-recursion {𝓀} {π“₯} {𝓦} {X} {Y} {A} = +-induction (Ξ» _ β†’ A) 𝟚 : 𝓀₀ Μ‡ 𝟚 = πŸ™ + πŸ™ pattern β‚€ = inl * pattern ₁ = inr * 𝟚-induction : (A : 𝟚 β†’ 𝓀 Μ‡ ) β†’ A β‚€ β†’ A ₁ β†’ (n : 𝟚) β†’ A n 𝟚-induction A aβ‚€ a₁ β‚€ = aβ‚€ 𝟚-induction A aβ‚€ a₁ ₁ = a₁ 𝟚-induction' : (A : 𝟚 β†’ 𝓀 Μ‡ ) β†’ A β‚€ β†’ A ₁ β†’ (n : 𝟚) β†’ A n 𝟚-induction' A aβ‚€ a₁ = +-induction A (πŸ™-induction (Ξ» (x : πŸ™) β†’ A (inl x)) aβ‚€) (πŸ™-induction (Ξ» (y : πŸ™) β†’ A (inr y)) a₁) {- Definition of dependent sum types -} record Ξ£ {𝓀 π“₯} {X : 𝓀 Μ‡} (Y : X β†’ π“₯ Μ‡ ) : 𝓀 βŠ” π“₯ Μ‡ where constructor _,_ field x : X y : Y x pr₁ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } β†’ Ξ£ Y β†’ X pr₁ (x , y) = x prβ‚‚ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } β†’ (z : Ξ£ Y) β†’ Y (pr₁ z) prβ‚‚ (x , y) = y -Ξ£ : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡ -Ξ£ X Y = Ξ£ Y syntax -Ξ£ X (Ξ» x β†’ y) = Ξ£ x κž‰ X , y Ξ£-induction : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {A : Ξ£ Y β†’ 𝓦 Μ‡ } β†’ ((x : X) (y : Y x) β†’ A (x , y)) β†’ ((x , y) : Ξ£ Y) β†’ A (x , y) Ξ£-induction g (x , y) = g x y curry : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {A : Ξ£ Y β†’ 𝓦 Μ‡ } β†’ (((x , y) : Ξ£ Y) β†’ A (x , y)) β†’ ((x : X) (y : Y x) β†’ A (x , y)) curry f x y = f (x , y) {- Binary product definition, using the dependent sum -} _Γ—_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡ X Γ— Y = Ξ£ x κž‰ X , Y {- Dependent product type definition -} Ξ  : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡ Ξ  {𝓀} {π“₯} {X} A = (x : X) β†’ A x -Ξ  : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡ -Ξ  X Y = Ξ  Y syntax -Ξ  A (Ξ» x β†’ b) = Ξ  x κž‰ A , b id : {X : 𝓀 Μ‡ } β†’ X β†’ X id x = x 𝑖𝑑 : (X : 𝓀 Μ‡ ) β†’ X β†’ X 𝑖𝑑 X = id _∘_ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : Y β†’ 𝓦 Μ‡ } β†’ ((y : Y) β†’ Z y) β†’ (f : X β†’ Y) β†’ (x : X) β†’ Z (f x) g ∘ f = Ξ» x β†’ g (f x) domain : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 Μ‡ domain {𝓀} {π“₯} {X} {Y} f = X codomain : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ π“₯ Μ‡ codomain {𝓀} {π“₯} {X} {Y} f = Y type-of : {X : 𝓀 Μ‡ } β†’ X β†’ 𝓀 Μ‡ type-of {𝓀} {X} x = X {- Defining the identity type -} data Id {𝓀} (X : 𝓀 Μ‡ ) : X β†’ X β†’ 𝓀 Μ‡ where refl : (x : X) β†’ Id X x x _≑_ : {X : 𝓀 Μ‡ } β†’ X β†’ X β†’ 𝓀 Μ‡ x ≑ y = Id _ x y 𝕁 : (X : 𝓀 Μ‡ ) (A : (x y : X) β†’ x ≑ y β†’ π“₯ Μ‡ ) β†’ ((x : X) β†’ A x x (refl x)) β†’ (x y : X) (p : x ≑ y) β†’ A x y p 𝕁 X A f x x (refl x) = f x transport : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} β†’ x ≑ y β†’ A x β†’ A y transport A (refl x) = 𝑖𝑑 (A x) lhs : {X : 𝓀 Μ‡ } {x y : X} β†’ x ≑ y β†’ X lhs {𝓀} {X} {x} {y} p = x rhs : {X : 𝓀 Μ‡ } {x y : X} β†’ x ≑ y β†’ X rhs {𝓀} {X} {x} {y} p = y refl_lhs : {X : 𝓀 Μ‡} {x y : X} β†’ (p : x ≑ y) β†’ (refl (lhs p) ≑ refl x) refl_lhs (refl x) = refl (refl x) _βˆ™_ : {X : 𝓀 Μ‡ } {x y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z p βˆ™ q = transport (lhs p ≑_) q p _⁻¹ : {X : 𝓀 Μ‡ } β†’ {x y : X} β†’ x ≑ y β†’ y ≑ x p ⁻¹ = transport (_≑ lhs p) p (refl (lhs p)) _βˆ™'_ : {X : 𝓀 Μ‡ } {x y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z p βˆ™' q = transport (_≑ rhs q) (p ⁻¹) q βˆ™agreement : {X : 𝓀 Μ‡ } {x y z : X} (p : x ≑ y) (q : y ≑ z) β†’ (p βˆ™' q) ≑ (p βˆ™ q) βˆ™agreement (refl x) (refl x) = refl (refl x) ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x x' : X} β†’ x ≑ x' β†’ f x ≑ f x' ap f {x} {x'} p = transport (Ξ» - β†’ f x ≑ f -) p (refl (f x)) _∼_ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ Ξ  A β†’ Ξ  A β†’ 𝓀 βŠ” π“₯ Μ‡ f ∼ g = βˆ€ x β†’ f x ≑ g x {- Lemma 2.1.4 from HoTT -} βˆ™assoc : {A : 𝓀 Μ‡} β†’ {w x y z : A} β†’ (p : w ≑ x) β†’ (q : x ≑ y) β†’ (r : y ≑ z) β†’ (p βˆ™ (q βˆ™ r)) ≑ ((p βˆ™ q) βˆ™ r) βˆ™assoc (refl w) (refl x) (refl y) = refl (refl x) invinv : {A : 𝓀 Μ‡} β†’ {x y : A} β†’ (p : x ≑ y) β†’ ((p ⁻¹) ⁻¹) ≑ p invinv (refl x) = refl (refl x) leftinv : {A : 𝓀 Μ‡} β†’ {x y : A} β†’ (p : x ≑ y) β†’ (((p ⁻¹) βˆ™ p) ≑ refl y) leftinv (refl x) = refl (refl x) rightinv : {A : 𝓀 Μ‡} β†’ {x y : A} β†’ (p : x ≑ y) β†’ ((p βˆ™ (p ⁻¹)) ≑ refl x) rightinv (refl x) = refl (refl x) ru : {A : 𝓀 Μ‡} β†’ {x y : A} β†’ (p : x ≑ y) β†’ ((p βˆ™ (refl y)) ≑ p) ru (refl x) = refl (refl x) lu : {A : 𝓀 Μ‡} β†’ {x y : A} β†’ (p : x ≑ y) β†’ (((refl x) βˆ™ p) ≑ p) lu (refl x) = refl (refl x)