module 1Lab.Inductive where open import 1Lab.Reflection open import 1Lab.Univalence open import 1Lab.Equiv open import 1Lab.Type hiding (case_of_ ; case_return_of_) open import 1Lab.Path {- Automation for applying induction principles ============================================ When working with mixed truncations/products/quotients, the relevant induction principles are often repeatedly applied in close succession, like in the snippet below. □-rec! λ { (a , b , w) → □-rec! (λ { (c , d , x) → inc (c , d , inc (a , x , w)) }) b } Applying these induction principles is entirely mechanical: like other mechanical processes, it's annoying to do by hand, generates ugly code, and causes a deep sense of existential uselessness. This module implements automation for automatically applying these eliminators "as far as possible", using overlapping instances. The Inductive class ------------------- The core of the implementation for rec!/elim! is the Inductive class, which is a slight misnomer. To support *nested* types with a single constructor, the Inductive class is applied to a section of the motive, not just base type. That is, if we want to simplify □ (□ A × □ (□ A)) → B ^~~~~~~~~~~~~~~~~ domain we don't look for an instance of `Inductive domain`, we look for an instance of `Inductive (domain → B)`. The relevant instances then manipulate the entire function type at once, much like Extensional. Writing rules ------------- Like Extensional, instances of 'Inductive' should be maximally lazy, so that the structural rules can fire as often as possible. That is, instead of writing ⦃ _ : ∀ {x} → Inductive (P (inc x)) ⦄ → Inductive (∀ x → P x) we write ⦃ _ : Inductive (∀ x → P (inc x)) ⦄ → Inductive (∀ x → P x) -} record Inductive {ℓ} (A : Type ℓ) ℓm : Type (ℓ ⊔ lsuc ℓm) where field methods : Type ℓm from : methods → A open Inductive private variable ℓ ℓ' ℓ'' ℓm : Level A B C : Type ℓ P Q R : A → Type ℓ instance -- The basic structural rules allow us to stop recurring (we can -- produce an A given an A) and to skip an argument, introducing a -- function type into the methods: Inductive-default : Inductive A (level-of A) Inductive-default .methods = _ Inductive-default .from x = x Inductive-Π : ⦃ _ : {x : A} → Inductive (P x) ℓm ⦄ → Inductive (∀ x → P x) (level-of A ⊔ ℓm) Inductive-Π ⦃ r ⦄ .methods = ∀ x → r {x} .methods Inductive-Π ⦃ r ⦄ .from f x = r .from (f x) {-# INCOHERENT Inductive-default #-} {-# OVERLAPPABLE Inductive-Π #-} -- Next, we have a rule for uncurrying pairs. This lets us handle types like -- □ (□ A × □ B) → C -- -- by factoring through -- -- □ (□ A × □ B) → C -- □ A × □ B → C -- □ A → □ B → C -- □ B → C Inductive-Σ : ∀ {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''} → ⦃ _ : Inductive ((x : A) (y : B x) → C x y) ℓm ⦄ → Inductive ((x : Σ A B) → C (x .fst) (x .snd)) ℓm Inductive-Σ ⦃ r ⦄ .methods = r .methods Inductive-Σ ⦃ r ⦄ .from f (x , y) = r .from f x y Inductive-Lift : {B : Lift ℓ A → Type ℓ'} → ⦃ _ : Inductive (∀ x → B (lift x)) ℓm ⦄ → Inductive (∀ x → B x) ℓm Inductive-Lift ⦃ i ⦄ = record { from = λ f (lift x) → i .from f x } -- However, we don't uncurry equivalences. Inductive-≃ : {C : A ≃ B → Type ℓ''} → Inductive (∀ x → C x) _ Inductive-≃ = Inductive-default {-# OVERLAPPING Inductive-≃ #-} -- For constructing (dependent) functions, there are two distinct prefix -- entry points: rec! and elim!. The difference is just in name, to -- provide a modicum of documentation. In addition, they have an -- explicit function type, so that the refine command will always -- introduce a question mark. rec! : ⦃ r : Inductive (A → B) ℓm ⦄ → r .methods → A → B rec! ⦃ r ⦄ = r .from elim! : ⦃ r : Inductive (∀ x → P x) ℓm ⦄ → r .methods → ∀ x → P x elim! ⦃ r ⦄ = r .from -- We also define versions of case_of_ and case_return_of_, shadowing -- those from 1Lab.Type, which insert a rec!/elim!. case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ⦃ r : Inductive (A → B) ℓm ⦄ → A → r .methods → B case x of f = rec! f x case_return_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} (x : A) (B : A → Type ℓ') ⦃ r : Inductive (∀ x → B x) ℓm ⦄ (f : r .methods) → B x case x return P of f = elim! f x {-# INLINE case_of_ #-} {-# INLINE case_return_of_ #-} -- For path!, we insist on returning a PathP type. This helps infer the -- line. path! : ∀ {B : I → Type ℓ} {f g} ⦃ r : Inductive (PathP B f g) ℓm ⦄ → r .methods → PathP B f g path! ⦃ r ⦄ = r .from instance Inductive-ua→ : ∀ {e : A ≃ B} {C : ∀ i → ua e i → Type ℓ} {f : ∀ a → C i0 a} {g : ∀ a → C i1 a} → ⦃ _ : Inductive ((x : A) → PathP (λ i → C i (ua-inc e x i)) (f x) (g (e .fst x))) ℓm ⦄ → Inductive (PathP (λ i → (x : ua e i) → C i x) f g) ℓm Inductive-ua→ ⦃ r ⦄ .methods = r .methods Inductive-ua→ ⦃ r ⦄ .from f = ua→ (λ a → r .from f a) Inductive-ua→' : ∀ {e : A ≃ B} {C : ∀ i → ua e i → Type ℓ} {f : ∀ {a} → C i0 a} {g : ∀ {a} → C i1 a} → ⦃ _ : Inductive ((x : A) → PathP (λ i → C i (ua-inc e x i)) (f {x}) (g {e .fst x})) ℓm ⦄ → Inductive (PathP (λ i → {x : ua e i} → C i x) f g) ℓm Inductive-ua→' ⦃ r ⦄ .methods = r .methods Inductive-ua→' ⦃ r ⦄ .from f = ua→' (λ a → r .from f a) Inductive-ua-path : ∀ {e : A ≃ B} {x : A} {y : B} → Inductive (PathP (λ i → ua e i) x y) (level-of B) Inductive-ua-path {e = e} {x} {y} .methods = e .fst x ≡ y Inductive-ua-path .from = path→ua-pathp _