{-# OPTIONS --without-K --type-in-type #-} open import Agda.Primitive renaming (_⊔_ to lmax) public open import Agda.Builtin.Sigma public open import Agda.Builtin.Unit public open import Agda.Builtin.Equality public open import Agda.Builtin.Nat renaming (Nat to ℕ) public open import Agda.Builtin.FromNat public open import Agda.Builtin.FromNeg public data TLevel : Set where ⟨-2⟩ : TLevel suc : (t : TLevel) → TLevel postulate magic : ∀ {i} {X : Set i} → X Type : Set₁ Type = Set -- a better name for Set data _⊔_ (A : Type) (B : Type) : Type where inl : A → A ⊔ B inr : B → A ⊔ B infixr 4 _⊔_ data ⊥ : Type where abort : {A : Type} → ⊥ → A abort () ¬_ : Type → Type ¬ A = A → ⊥ {- START of Agda hack to write numerals directly -} instance Numℕ : Number ℕ Number.Constraint Numℕ _ = ⊤ Number.fromNat Numℕ n = n NumTLevel : Number TLevel Number.Constraint NumTLevel _ = ⊤ Number.fromNat NumTLevel k = natToTLevel k where natToTLevel : ∀ ℕ → {{_ : ⊤}} → TLevel natToTLevel 0 = suc (suc ⟨-2⟩) natToTLevel (suc n) = suc (natToTLevel n) NegTLevel : Negative TLevel Negative.Constraint NegTLevel 0 = ⊤ Negative.Constraint NegTLevel 1 = ⊤ Negative.Constraint NegTLevel 2 = ⊤ Negative.Constraint NegTLevel _ = ⊥ Negative.fromNeg NegTLevel 0 = suc (suc ⟨-2⟩) Negative.fromNeg NegTLevel 1 = suc ⟨-2⟩ Negative.fromNeg NegTLevel 2 = ⟨-2⟩ Negative.fromNeg NegTLevel (suc (suc (suc _))) ⦃()⦄ {- END of the Agda hack to write numerals -} ap : ∀ {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y ap f refl = refl {- groupoidal aspects -} _∙_ : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z refl ∙ q = q infixr 80 _∙_ !_ : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x ! refl = refl infixr 100 !_ ∙-unit-r : ∀ {A : Type} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q ∙-unit-r refl = refl ∙-unit-l : ∀ {A : Type} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q ∙-unit-l q = refl !-inv-l : ∀ {A : Type} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl !-inv-l refl = refl !-inv-r : ∀ {A : Type} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl !-inv-r refl = refl !-! : ∀ {A : Type} {x y : A} (p : x ≡ y) → ! (! p) ≡ p !-! refl = refl ∙-assoc : ∀ {A : Type} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r) ∙-assoc refl q r = refl {- functorial aspects -} ap-∙ : ∀ {A B : Type} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q ap-∙ f refl q = refl ap-! : ∀ {A B : Type} (f : A → B) {x y : A} (p : x ≡ y) → ap f (! p) ≡ ! (ap f p) ap-! f refl = refl {- dependent paths -} PathOver : ∀ {A : Type} (C : A → Type) {x y} → x ≡ y → C x → C y → Type PathOver C refl cx cy = cx ≡ cy infix 30 PathOver syntax PathOver B p u v = u ≡ v [ B ↓ p ] apd : ∀ {A : Type} (C : A → Type) (f : (a : A) → C a) {x y : A} (p : x ≡ y) → f x ≡ f y [ C ↓ p ] apd C f refl = refl