{-# OPTIONS --without-K #-} open import Agda.Primitive open import 1-equality open import 2-composition open import 2-ski open import 3-ap open import 4-homotopy open import 4-transport open import 5-qip open import 6-equivalence open import 7-dependentpairs elim[Π≡Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → f ≡ g → f ∼ g elim[Π≡Π] refl = refl[∼] postulate intr[Π≡Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → f ∼ g → f ≡ g postulate weakuniq[Π≡Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f : Π A B} → (intr[Π≡Π] ∘ elim[Π≡Π]) ∼ id' (f ≡ f) uniq[Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → intr[Π≡Π] ∘ elim[Π≡Π] ∼ id' (f ≡ g) uniq[Π] {f = f} {g = f} refl = weakuniq[Π≡Π] refl postulate elim[Π≡Π]·is·epic : {ℓ₁ ℓ₂ ℓ₃ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → {C : Set ℓ₃} → {F G : (f ∼ g) → C} → (F ∘ elim[Π≡Π] ≡ G ∘ elim[Π≡Π]) → F ≡ G comp[Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → elim[Π≡Π] ∘ intr[Π≡Π] ∼ id' (f ∼ g) comp[Π] = elim[Π≡Π] (elim[Π≡Π]·is·epic (intr[Π≡Π] (elim[Π≡Π] (ass[∘] elim[Π≡Π] intr[Π≡Π] elim[Π≡Π]) •[∼] (elim[Π≡Π] ∘∼ uniq[Π])))) ∼≃≡ : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → (f ∼ g) ≃ (f ≡ g) ∼≃≡ = QIP·to·≃ QIP[ intr[Π≡Π] , elim[Π≡Π] , uniq[Π] , comp[Π] ] comp·refl[Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f : Π A B} → intr[Π≡Π] refl[∼] ≡ refl' f comp·refl[Π] = uniq[Π] refl comp·sym[Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g : Π A B} → (α : f ≡ g) → intr[Π≡Π] (sym[∼] (elim[Π≡Π] α)) ≡ sym α comp·sym[Π] refl = uniq[Π] refl comp·•[Π] : {ℓ₁ ℓ₂ : Level} → {A : Set ℓ₁} → {B : A → Set ℓ₂} → {f g h : Π A B} → (α : f ≡ g) → (β : g ≡ h) → intr[Π≡Π] (elim[Π≡Π] α •[∼] elim[Π≡Π] β) ≡ α • β comp·•[Π] refl refl = uniq[Π] refl comp·transport[→] : {ℓ₁ ℓ₂ ℓ₃ : Level} → {X : Set ℓ₁} → {A : X → Set ℓ₂} → {B : X → Set ℓ₃} → {x₁ x₂ : X} → (p : x₁ ≡ x₂) → (f : A x₁ → B x₁) → let A→B = λ x → (A x → B x) g = λ a → f (transport A (sym p) a) in transport A→B p f ≡ λ a → transport B p (g a) comp·transport[→] refl _ = intr[Π≡Π] refl[∼] comp·transport[Π] : {ℓ₁ ℓ₂ ℓ₃ : Level} → {X : Set ℓ₁} → {A : X → Set ℓ₂} → {B : (x : X) → A x → Set ℓ₃} → {x₁ x₂ : X} → (p : x₁ ≡ x₂) → (f : Π (A x₁) λ a → B x₁ a) → (a : A x₂) → let P = λ x → Π (A x) (B x) Q = λ {[ w₁ , w₂ ] → B w₁ w₂} q = sym (intr[Σ≡Σ] [ sym p , refl ]) g = λ a → f (transport A (sym p) a) in transport P p f a ≡ transport Q q (g a) comp·transport[Π] refl f a = refl Lemma·2·9·6 : {ℓ₁ ℓ₂ ℓ₃ : Level} → {X : Set ℓ₁} → {A : X → Set ℓ₂} → {B : X → Set ℓ₃} → {x₁ x₂ : X} → (p : x₁ ≡ x₂) → (f : A x₁ → B x₁) → (g : A x₂ → B x₂) → let Aᵀ : A x₁ → A x₂ Aᵀ = transport A p Bᵀ : B x₁ → B x₂ Bᵀ = transport B p A→B = λ x → (A x → B x) A→Bᵀ : A→B x₁ → A→B x₂ A→Bᵀ = transport A→B p in (A→Bᵀ f ≡ g) ≃ (Bᵀ ∘ f ≡ g ∘ Aᵀ) Lemma·2·9·6 {A = A} {B = B} {x₁ = x₁} {x₂ = x₂} refl f g = ≃[ id , id , id , refl[∼] , refl[∼] ] Lemma·2·9·7 : {ℓ₁ ℓ₂ ℓ₃ : Level} → {X : Set ℓ₁} → {A : X → Set ℓ₂} → {B : (Σ X A) → Set ℓ₃} → {x₁ x₂ : X} → (p : x₁ ≡ x₂) → (f : (a : A x₁) → B [ x₁ , a ] ) → (g : (a : A x₂) → B [ x₂ , a ] ) → let Aᵀ : A x₁ → A x₂ Aᵀ = transport A p Bᵀ : (a : A x₁) → B [ x₁ , a ] → B [ x₂ , Aᵀ a ] Bᵀ = λ a → transport B (path·lift A p a) ΠAB : (x : X) → Set (ℓ₂ ⊔ ℓ₃) ΠAB = λ x → (a : A x) → B [ x , a ] ΠABᵀ : ΠAB x₁ → ΠAB x₂ ΠABᵀ = transport ΠAB p in (ΠABᵀ f ≡ g) ≃ (Bᵀ ∘' f ∼ g ∘ Aᵀ) Lemma·2·9·7 refl f g = QIP·to·≃ QIP[ elim[Π≡Π] , intr[Π≡Π] , comp[Π] , uniq[Π] ] sym∘sym≡id : {ℓ : Level} → {A : Set ℓ} → {x y : A} → sym ∘ sym ≡ id' (x ≡ y) sym∘sym≡id = intr[Π≡Π] λ { refl → refl } ΠΠ≃Σ→ : {ℓ₁ ℓ₂ ℓ₃ : Level} → (X : Set ℓ₁) → (Y : X → Set ℓ₂) → ((x : X) → Y x → Set ℓ₃) ≃ ((Σ X Y) → Set ℓ₃) ΠΠ≃Σ→ X Y = QIP·to·≃ QIP[ (λ f → λ { [ x , y ] → f x y}) , (λ f → λ { x y → f [ x , y ]}) , refl[∼] , refl[∼] ]