{-# OPTIONS --without-K #-} {- The above line turns off the axiom K. The Axiom K is equivalent to UIP and would turn our identification types into "identification types with UIP". We do not want that. -} 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 instance Numℕ : Number ℕ Number.Constraint Numℕ _ = ⊤ Number.fromNat Numℕ n = n 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 ¬_ : Type → Type ¬ A = A → ⊥ 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 {- Part I: general facts about homotopy levels and truncation levels -} {- homotopy levels | truncation levels (h-levels) | -----------------+------------------- 0 | -2 1 | -1 2 | 0 ... | ... -} {- we like truncation levels more today -} data TLevel : Type where ⟨-2⟩ : TLevel suc : (t : TLevel) → TLevel {- START of Agda hack to write numerals directly -} instance 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 -} {- resuming what we did last week... -} is-contr : Type → Type is-contr A = Σ A (λ x → (y : A) → x ≡ y) has-level : TLevel → Type → Type has-level ⟨-2⟩ A = is-contr A has-level (suc n) A = (x y : A) → has-level n (x ≡ y) is-prop : Type → Type is-prop = has-level -1 -- this was "has-level 1" last week is-set : Type → Type is-set = has-level 0 -- this was "has-level 2" last week {- it turns out this is equivalent to is-prop! -} has-all-paths : Type → Type has-all-paths A = (x y : A) → x ≡ y {- this is the easy direction -} prop-has-all-paths : ∀ {A : Type} → is-prop A → has-all-paths A prop-has-all-paths propA x y = fst (propA x y) {- this was the end of the lecture on 2020/02/13 -} contr-has-all-paths : ∀ {A : Type} → is-contr A → has-all-paths A contr-has-all-paths contrA x y = ! (snd contrA x) ∙ snd contrA y {- This is difficult! Do Homework 2 to digest this part. -} all-paths-is-prop : ∀ {A : Type} → has-all-paths A → is-prop A all-paths-is-prop {A} c x y = (center x y , canon-path) where center : (x y : A) → x ≡ y center x y = ! (c x x) ∙ c x y canon-path : {x y : A} (p : x ≡ y) → center x y ≡ p canon-path {x} refl = !-inv-l (c x x) raise-level : ∀ {A : Type} (n : TLevel) → has-level n A → has-level (suc n) A raise-level ⟨-2⟩ contrA = all-paths-is-prop (contr-has-all-paths contrA) raise-level = magic {- PART II: Paths structure of specific types -} record is-equiv {A B : Type} (f : A → B) : Type where field g : B → A f-g : ∀ (b : B) → f (g b) ≡ b g-f : ∀ (a : A) → g (f a) ≡ a adj : ∀ (a : A) → ap f (g-f a) ≡ f-g (f a) infix 30 _≃_ _≃_ : Type → Type → Type A ≃ B = Σ (A → B) is-equiv {- quasi-inverses -> equivalences -} is-eq : ∀ {A B : Type} (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x) → is-equiv f is-eq {A} {B} f g f-g g-f = record {g = g; f-g = f-g'; g-f = g-f; adj = adj} where abstract {- adjusting f-g -} f-g' : (y : B) → f (g y) ≡ y f-g' b = ! (ap (λ y → f (g y)) (f-g b)) ∙ ap f (g-f (g b)) ∙ f-g b {- you can prove this with adjusted f-g -} postulate adj : (x : A) → ap f (g-f x) ≡ f-g' (f x) equiv : ∀ {A B : Type} (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x) → A ≃ B equiv f g f-g g-f = f , is-eq f g f-g g-f ≡⊤ : (x y : ⊤) → Type ≡⊤ _ _ = ⊤ ≡⊤-econv : ∀ (x y : ⊤) → (x ≡ y) ≃ (≡⊤ x y) ≡⊤-econv x y = equiv f g f-g g-f where f : x ≡ y → ≡⊤ x y f _ = tt g : ≡⊤ x y → x ≡ y g _ = refl f-g : ∀ (p : ≡⊤ x y) → f (g p) ≡ p f-g _ = refl g-f : ∀ (p : x ≡ y) → g (f p) ≡ p g-f refl = refl ≡⊥ : (x y : ⊥) → Type ≡⊥ _ _ = ⊥ ≡⊥-econv : ∀ (x y : ⊥) → (x ≡ y) ≃ (≡⊥ x y) ≡⊥-econv () _×_ : Type → Type → Type A × B = Σ A (λ _ → B) ≡× : ∀ {A B : Type} (x y : A × B) → Type ≡× (x₁ , x₂) (y₁ , y₂) = (x₁ ≡ y₁) × (x₂ ≡ y₂) ≡×-econv : ∀ {A B : Type} (x y : A × B) → (x ≡ y) ≃ (≡× x y) ≡×-econv x y = equiv f g f-g g-f where f : x ≡ y → ≡× x y f refl = refl , refl g : ≡× x y → x ≡ y g (refl , refl) = refl f-g : ∀ (p : ≡× x y) → f (g p) ≡ p f-g (refl , refl) = refl g-f : ∀ (p : x ≡ y) → g (f p) ≡ p g-f refl = refl {- the lecture on 2/20 stopped here -} {- dependent paths -} PathOver : ∀ {A : Type} (B : A → Type) {x y} → x ≡ y → B x → B y → Type PathOver B refl u v = u ≡ v infix 30 PathOver syntax PathOver B p u v = u ≡ v [ B ↓ p ] ≡Σ : ∀ {A : Type} {B : A → Type} → (x y : Σ A B) → Type ≡Σ {B = B} (x1 , x2) (y1 , y2) = magic {- Bonus exercise: state and prove something analogous to ≡×-econv -} ≡⊔ : ∀ {A B : Type} (x y : A ⊔ B) → Type ≡⊔ = magic {- Bonus exercise: state and prove something analogous to ≡×-econv -} ≡ℕ : ∀ {A B : Type} (x y : ℕ) → Type ≡ℕ = magic {- Bonus^1 exercise: state and prove something analogous to ≡×-econv -} {- Bonus^2 exercise: show that ∀ (n : ℕ) → ¬ (0 ≡ suc n) -} {- Bonus^3 exercise: show that ∀ (n m : ℕ) → (n ≡ m) ⊔ (¬ (n ≡ m)) -} {- Bonus^4 exercise: combined with Homework 2, show that "is-set ℕ" -} {- PART III: more operators for identifications -} {- more about path-overs -} transport : ∀ {A : Type} (B : A → Type) {x y : A} (p : x ≡ y) → B x → B y transport = magic from-transp : ∀ {A : Type} (B : A → Type) {x y : A} (p : x ≡ y) {u : B x} {v : B y} → (transport B p u ≡ v) → u ≡ v [ B ↓ p ] from-transp = magic {- going back to J -} J : ∀ {A : Type} {x : A} (B : (x' : A) → x ≡ x' → Type) (refl* : B x refl) {x' : A} (p : x ≡ x') → B x' p J = magic {- this is not provable --without-K -} K : ∀ {A : Type} {x : A} (B : x ≡ x → Type) (refl* : B refl) {x' : A} (p : x ≡ x) → B p K = magic