Last active
October 4, 2016 23:26
-
-
Save mietek/48b666de614bf01a51c152aeb12de556 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module Experiments where | |
| open import BasicIS4.Syntax.DyadicGentzen public | |
| -- A strict total order on types. | |
| mutual | |
| infix 3 _<ᵀˣᵀ_ | |
| _<ᵀˣᵀ_ : Ty × Ty → Ty × Ty → Set | |
| A , B <ᵀˣᵀ A′ , B′ = A <ᵀ A′ ⊎ A ≡ A′ × B <ᵀ B′ | |
| infix 3 _<ᵀ_ | |
| _<ᵀ_ : Ty → Ty → Set | |
| α P <ᵀ α P′ = P <ᵅ P′ | |
| α P <ᵀ A′ ▻ B′ = 𝟙 | |
| α P <ᵀ □ A′ = 𝟙 | |
| α P <ᵀ A′ ∧ B′ = 𝟙 | |
| α P <ᵀ ⊤ = 𝟙 | |
| A ▻ B <ᵀ α P′ = 𝟘 | |
| A ▻ B <ᵀ A′ ▻ B′ = A , B <ᵀˣᵀ A′ , B′ | |
| A ▻ B <ᵀ □ A′ = 𝟙 | |
| A ▻ B <ᵀ A′ ∧ B′ = 𝟙 | |
| A ▻ B <ᵀ ⊤ = 𝟙 | |
| □ A <ᵀ α P′ = 𝟘 | |
| □ A <ᵀ A′ ▻ B′ = 𝟘 | |
| □ A <ᵀ □ A′ = A <ᵀ A′ | |
| □ A <ᵀ A′ ∧ B′ = 𝟙 | |
| □ A <ᵀ ⊤ = 𝟙 | |
| A ∧ B <ᵀ α P′ = 𝟘 | |
| A ∧ B <ᵀ A′ ▻ B′ = 𝟘 | |
| A ∧ B <ᵀ □ A′ = 𝟘 | |
| A ∧ B <ᵀ A′ ∧ B′ = A , B <ᵀˣᵀ A′ , B′ | |
| A ∧ B <ᵀ ⊤ = 𝟙 | |
| ⊤ <ᵀ α P′ = 𝟘 | |
| ⊤ <ᵀ A′ ▻ B′ = 𝟘 | |
| ⊤ <ᵀ □ A′ = 𝟘 | |
| ⊤ <ᵀ A′ ∧ B′ = 𝟘 | |
| ⊤ <ᵀ ⊤ = 𝟘 | |
| infix 3 _≮ᵀ_ | |
| _≮ᵀ_ : Ty → Ty → Set | |
| A ≮ᵀ A′ = Not (A <ᵀ A′) | |
| infix 3 _≮ᵀˣᵀ_ | |
| _≮ᵀˣᵀ_ : Ty × Ty → Ty × Ty → Set | |
| A , B ≮ᵀˣᵀ A′ , B′ = Not (A , B <ᵀˣᵀ A′ , B′) | |
| trans<ᵀ : Transitive _<ᵀ_ | |
| trans<ᵀ {α P} {α P′} {α P″} p q = trans<ᵅ p q | |
| trans<ᵀ {α P} {α P′} {A″ ▻ B″} p q = ∙ | |
| trans<ᵀ {α P} {α P′} {□ A″} p q = ∙ | |
| trans<ᵀ {α P} {α P′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {α P} {α P′} {⊤} p q = ∙ | |
| trans<ᵀ {α P} {A′ ▻ B′} {α P″} p () | |
| trans<ᵀ {α P} {A′ ▻ B′} {A″ ▻ B″} p q = ∙ | |
| trans<ᵀ {α P} {A′ ▻ B′} {□ A″} p q = ∙ | |
| trans<ᵀ {α P} {A′ ▻ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {α P} {A′ ▻ B′} {⊤} p q = ∙ | |
| trans<ᵀ {α P} {□ A′} {α P″} p () | |
| trans<ᵀ {α P} {□ A′} {A″ ▻ B″} p () | |
| trans<ᵀ {α P} {□ A′} {□ A″} p q = ∙ | |
| trans<ᵀ {α P} {□ A′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {α P} {□ A′} {⊤} p q = ∙ | |
| trans<ᵀ {α P} {A′ ∧ B′} {α P″} p () | |
| trans<ᵀ {α P} {A′ ∧ B′} {A″ ▻ B″} p () | |
| trans<ᵀ {α P} {A′ ∧ B′} {□ A″} p () | |
| trans<ᵀ {α P} {A′ ∧ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {α P} {A′ ∧ B′} {⊤} p q = ∙ | |
| trans<ᵀ {α P} {⊤} {α P″} p () | |
| trans<ᵀ {α P} {⊤} {A″ ▻ B″} p () | |
| trans<ᵀ {α P} {⊤} {□ A″} p () | |
| trans<ᵀ {α P} {⊤} {A″ ∧ B″} p () | |
| trans<ᵀ {α P} {⊤} {⊤} p q = ∙ | |
| trans<ᵀ {A ▻ B} {α P′} {α P″} () q | |
| trans<ᵀ {A ▻ B} {α P′} {A″ ▻ B″} () q | |
| trans<ᵀ {A ▻ B} {α P′} {□ A″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {α P′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {α P′} {⊤} p q = ∙ | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {α P″} p () | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {A″ ▻ B″} (ι₁ A<A′) (ι₁ A′<A″) = ι₁ (trans<ᵀ {A} {A′} {A″} A<A′ A′<A″) | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {.A′ ▻ B″} (ι₁ A<A′) (ι₂ (refl , B′<B″)) = ι₁ A<A′ | |
| trans<ᵀ {A ▻ B} {.A ▻ B′} {A″ ▻ B″} (ι₂ (refl , B<B′)) (ι₁ A<A″) = ι₁ A<A″ | |
| trans<ᵀ {A ▻ B} {.A ▻ B′} {.A ▻ B″} (ι₂ (refl , B<B′)) (ι₂ (refl , B′<B″)) = ι₂ (refl , trans<ᵀ {B} {B′} {B″} B<B′ B′<B″) | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {□ A″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {A′ ▻ B′} {⊤} p q = ∙ | |
| trans<ᵀ {A ▻ B} {□ A′} {α P″} p () | |
| trans<ᵀ {A ▻ B} {□ A′} {A″ ▻ B″} p () | |
| trans<ᵀ {A ▻ B} {□ A′} {□ A″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {□ A′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {□ A′} {⊤} p q = ∙ | |
| trans<ᵀ {A ▻ B} {A′ ∧ B′} {α P″} p () | |
| trans<ᵀ {A ▻ B} {A′ ∧ B′} {A″ ▻ B″} p () | |
| trans<ᵀ {A ▻ B} {A′ ∧ B′} {□ A″} p () | |
| trans<ᵀ {A ▻ B} {A′ ∧ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {A ▻ B} {A′ ∧ B′} {⊤} p q = ∙ | |
| trans<ᵀ {A ▻ B} {⊤} {α P″} p () | |
| trans<ᵀ {A ▻ B} {⊤} {A″ ▻ B″} p () | |
| trans<ᵀ {A ▻ B} {⊤} {□ A″} p () | |
| trans<ᵀ {A ▻ B} {⊤} {A″ ∧ B″} p () | |
| trans<ᵀ {A ▻ B} {⊤} {⊤} p q = ∙ | |
| trans<ᵀ {□ A} {α P′} {α P″} () q | |
| trans<ᵀ {□ A} {α P′} {A″ ▻ B″} () q | |
| trans<ᵀ {□ A} {α P′} {□ A″} () q | |
| trans<ᵀ {□ A} {α P′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {□ A} {α P′} {⊤} p q = ∙ | |
| trans<ᵀ {□ A} {A′ ▻ B′} {α P″} p () | |
| trans<ᵀ {□ A} {A′ ▻ B′} {A″ ▻ B″} () q | |
| trans<ᵀ {□ A} {A′ ▻ B′} {□ A″} () q | |
| trans<ᵀ {□ A} {A′ ▻ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {□ A} {A′ ▻ B′} {⊤} p q = ∙ | |
| trans<ᵀ {□ A} {□ A′} {α P″} p () | |
| trans<ᵀ {□ A} {□ A′} {A″ ▻ B″} p () | |
| trans<ᵀ {□ A} {□ A′} {□ A″} p q = trans<ᵀ {A} {A′} {A″} p q | |
| trans<ᵀ {□ A} {□ A′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {□ A} {□ A′} {⊤} p q = ∙ | |
| trans<ᵀ {□ A} {A′ ∧ B′} {α P″} p () | |
| trans<ᵀ {□ A} {A′ ∧ B′} {A″ ▻ B″} p () | |
| trans<ᵀ {□ A} {A′ ∧ B′} {□ A″} p () | |
| trans<ᵀ {□ A} {A′ ∧ B′} {A″ ∧ B″} p q = ∙ | |
| trans<ᵀ {□ A} {A′ ∧ B′} {⊤} p q = ∙ | |
| trans<ᵀ {□ A} {⊤} {α P″} p () | |
| trans<ᵀ {□ A} {⊤} {A″ ▻ B″} p () | |
| trans<ᵀ {□ A} {⊤} {□ A″} p () | |
| trans<ᵀ {□ A} {⊤} {A″ ∧ B″} p () | |
| trans<ᵀ {□ A} {⊤} {⊤} p q = ∙ | |
| trans<ᵀ {A ∧ B} {α P′} {α P″} () q | |
| trans<ᵀ {A ∧ B} {α P′} {A″ ▻ B″} () q | |
| trans<ᵀ {A ∧ B} {α P′} {□ A″} () q | |
| trans<ᵀ {A ∧ B} {α P′} {A″ ∧ B″} () q | |
| trans<ᵀ {A ∧ B} {α P′} {⊤} p q = ∙ | |
| trans<ᵀ {A ∧ B} {A′ ▻ B′} {α P″} p () | |
| trans<ᵀ {A ∧ B} {A′ ▻ B′} {A″ ▻ B″} () q | |
| trans<ᵀ {A ∧ B} {A′ ▻ B′} {□ A″} () q | |
| trans<ᵀ {A ∧ B} {A′ ▻ B′} {A″ ∧ B″} () q | |
| trans<ᵀ {A ∧ B} {A′ ▻ B′} {⊤} p q = ∙ | |
| trans<ᵀ {A ∧ B} {□ A′} {α P″} p () | |
| trans<ᵀ {A ∧ B} {□ A′} {A″ ▻ B″} p () | |
| trans<ᵀ {A ∧ B} {□ A′} {□ A″} () q | |
| trans<ᵀ {A ∧ B} {□ A′} {A″ ∧ B″} () q | |
| trans<ᵀ {A ∧ B} {□ A′} {⊤} p q = ∙ | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {α P″} p () | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {A″ ▻ B″} p () | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {□ A″} p () | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {A″ ∧ B″} (ι₁ A<A′) (ι₁ A′<A″) = ι₁ (trans<ᵀ {A} {A′} {A″} A<A′ A′<A″) | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {.A′ ∧ B″} (ι₁ A<A′) (ι₂ (refl , B′<B″)) = ι₁ A<A′ | |
| trans<ᵀ {A ∧ B} {.A ∧ B′} {A″ ∧ B″} (ι₂ (refl , B<B′)) (ι₁ A<A″) = ι₁ A<A″ | |
| trans<ᵀ {A ∧ B} {.A ∧ B′} {.A ∧ B″} (ι₂ (refl , B<B′)) (ι₂ (refl , B′<B″)) = ι₂ (refl , trans<ᵀ {B} {B′} {B″} B<B′ B′<B″) | |
| trans<ᵀ {A ∧ B} {A′ ∧ B′} {⊤} p q = ∙ | |
| trans<ᵀ {A ∧ B} {⊤} {α P″} p () | |
| trans<ᵀ {A ∧ B} {⊤} {A″ ▻ B″} p () | |
| trans<ᵀ {A ∧ B} {⊤} {□ A″} p () | |
| trans<ᵀ {A ∧ B} {⊤} {A″ ∧ B″} p () | |
| trans<ᵀ {A ∧ B} {⊤} {⊤} p q = ∙ | |
| trans<ᵀ {⊤} {α P′} {α P″} () q | |
| trans<ᵀ {⊤} {α P′} {A″ ▻ B″} () q | |
| trans<ᵀ {⊤} {α P′} {□ A″} () q | |
| trans<ᵀ {⊤} {α P′} {A″ ∧ B″} () q | |
| trans<ᵀ {⊤} {α P′} {⊤} () q | |
| trans<ᵀ {⊤} {A′ ▻ B′} {α P″} p () | |
| trans<ᵀ {⊤} {A′ ▻ B′} {A″ ▻ B″} () q | |
| trans<ᵀ {⊤} {A′ ▻ B′} {□ A″} () q | |
| trans<ᵀ {⊤} {A′ ▻ B′} {A″ ∧ B″} () q | |
| trans<ᵀ {⊤} {A′ ▻ B′} {⊤} () q | |
| trans<ᵀ {⊤} {□ A′} {α P″} p () | |
| trans<ᵀ {⊤} {□ A′} {A″ ▻ B″} p () | |
| trans<ᵀ {⊤} {□ A′} {□ A″} () q | |
| trans<ᵀ {⊤} {□ A′} {A″ ∧ B″} () q | |
| trans<ᵀ {⊤} {□ A′} {⊤} () q | |
| trans<ᵀ {⊤} {A′ ∧ B′} {α P″} p () | |
| trans<ᵀ {⊤} {A′ ∧ B′} {A″ ▻ B″} p () | |
| trans<ᵀ {⊤} {A′ ∧ B′} {□ A″} p () | |
| trans<ᵀ {⊤} {A′ ∧ B′} {A″ ∧ B″} () q | |
| trans<ᵀ {⊤} {A′ ∧ B′} {⊤} () q | |
| trans<ᵀ {⊤} {⊤} {α P″} p () | |
| trans<ᵀ {⊤} {⊤} {A″ ▻ B″} p () | |
| trans<ᵀ {⊤} {⊤} {□ A″} p () | |
| trans<ᵀ {⊤} {⊤} {A″ ∧ B″} p () | |
| trans<ᵀ {⊤} {⊤} {⊤} () () | |
| ≢→αP≢αP′ : ∀ {P P′} → P ≢ P′ → α P ≢ α P′ | |
| ≢→αP≢αP′ P≢P′ refl = refl ↯ P≢P′ | |
| ≢→A▻B≢A▻B′ : ∀ {A B B′} → B ≢ B′ → A ▻ B ≢ A ▻ B′ | |
| ≢→A▻B≢A▻B′ B≢B′ refl = refl ↯ B≢B′ | |
| ≢→A▻B≢A′▻B′ : ∀ {A A′ B B′} → A ≢ A′ → A ▻ B ≢ A′ ▻ B′ | |
| ≢→A▻B≢A′▻B′ A≢A′ refl = refl ↯ A≢A′ | |
| ≢→□A≢□A′ : ∀ {A A′} → A ≢ A′ → □ A ≢ □ A′ | |
| ≢→□A≢□A′ A≢A′ refl = refl ↯ A≢A′ | |
| ≢→A∧B≢A∧B′ : ∀ {A B B′} → B ≢ B′ → A ∧ B ≢ A ∧ B′ | |
| ≢→A∧B≢A∧B′ B≢B′ refl = refl ↯ B≢B′ | |
| ≢→A∧B≢A′∧B′ : ∀ {A A′ B B′} → A ≢ A′ → A ∧ B ≢ A′ ∧ B′ | |
| ≢→A∧B≢A′∧B′ A≢A′ refl = refl ↯ A≢A′ | |
| mutual | |
| irrefl<ᵀ : Irreflexive _<ᵀ_ | |
| irrefl<ᵀ (α P) = irrefl<ᵅ P | |
| irrefl<ᵀ (A ▻ B) = irrefl<ᵀˣᵀ (A , B) | |
| irrefl<ᵀ (□ A) = irrefl<ᵀ A | |
| irrefl<ᵀ (A ∧ B) = irrefl<ᵀˣᵀ (A , B) | |
| irrefl<ᵀ ⊤ = I | |
| irrefl<ᵀˣᵀ : Irreflexive _<ᵀˣᵀ_ | |
| irrefl<ᵀˣᵀ (A , B) (ι₁ A<A) = A<A ↯ irrefl<ᵀ A | |
| irrefl<ᵀˣᵀ (A , B) (ι₂ (refl , B<B)) = B<B ↯ irrefl<ᵀ B | |
| ≮→AB≮AB′ : ∀ {A B B′} → B ≮ᵀ B′ → A , B ≮ᵀˣᵀ A , B′ | |
| ≮→AB≮AB′ {A} B≮B′ (ι₁ A<A) = A<A ↯ irrefl<ᵀ A | |
| ≮→AB≮AB′ {A} B≮B′ (ι₂ (refl , B<B′)) = B<B′ ↯ B≮B′ | |
| ≰→AB≮A′B′ : ∀ {A A′ B B′} → A ≮ᵀ A′ → A ≢ A′ → A , B ≮ᵀˣᵀ A′ , B′ | |
| ≰→AB≮A′B′ A≮A′ A≢A′ (ι₁ A<A′) = A<A′ ↯ A≮A′ | |
| ≰→AB≮A′B′ A≮A′ A≢A′ (ι₂ (refl , B<B′)) = refl ↯ A≢A′ | |
| tri<ᵀ : Trichotomous _≡_ _<ᵀ_ | |
| tri<ᵀ (α P) (α P′) with tri<ᵅ P P′ | |
| tri<ᵀ (α P) (α P′) | τ₍ P<P′ P≢P′ P′≮P = τ₍ P<P′ (≢→αP≢αP′ P≢P′) P′≮P | |
| tri<ᵀ (α P) (α .P) | τ₌ P≮P′ refl P′≮P = τ₌ P≮P′ refl P′≮P | |
| tri<ᵀ (α P) (α P′) | τ₎ P≮P′ P≢P′ P′<P = τ₎ P≮P′ (≢→αP≢αP′ P≢P′) P′<P | |
| tri<ᵀ (α P) (A′ ▻ B′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (α P) (□ A′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (α P) (A′ ∧ B′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (α P) ⊤ = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (A ▻ B) (α P′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (A ▻ B) (A′ ▻ B′) with tri<ᵀ A A′ | tri<ᵀ B B′ | |
| tri<ᵀ (A ▻ B) (A′ ▻ B′) | τ₍ A<A′ A≢A′ A′≮A | _ = τ₍ (ι₁ A<A′) (≢→A▻B≢A′▻B′ A≢A′) (≰→AB≮A′B′ {B = B′} A′≮A (sym≢ A≢A′)) | |
| tri<ᵀ (A ▻ B) (.A ▻ B′) | τ₌ A≮A′ refl A′≮A | τ₍ B<B′ B≢B′ B′≮B = τ₍ (ι₂ (refl , B<B′)) (≢→A▻B≢A▻B′ B≢B′) (≮→AB≮AB′ {B = B′} B′≮B) | |
| tri<ᵀ (A ▻ B) (.A ▻ .B) | τ₌ A≮A′ refl A′≮A | τ₌ B≮B′ refl B′≮B = τ₌ (irrefl<ᵀˣᵀ (A , B)) refl (irrefl<ᵀˣᵀ (A , B)) | |
| tri<ᵀ (A ▻ B) (.A ▻ B′) | τ₌ A≮A′ refl A′≮A | τ₎ B≮B′ B≢B′ B′<B = τ₎ (≮→AB≮AB′ {B = B} B≮B′) (≢→A▻B≢A▻B′ B≢B′) (ι₂ (refl , B′<B)) | |
| tri<ᵀ (A ▻ B) (A′ ▻ B′) | τ₎ A≮A′ A≢A′ A′<A | _ = τ₎ (≰→AB≮A′B′ {B = B} A≮A′ A≢A′) (≢→A▻B≢A′▻B′ A≢A′) (ι₁ A′<A) | |
| tri<ᵀ (A ▻ B) (□ A′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (A ▻ B) (A′ ∧ B′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (A ▻ B) ⊤ = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (□ A) (α P′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (□ A) (A′ ▻ B′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (□ A) (□ A′) with tri<ᵀ A A′ | |
| tri<ᵀ (□ A) (□ A′) | τ₍ A<A′ A≢A′ A′≮A = τ₍ A<A′ (≢→□A≢□A′ A≢A′) A′≮A | |
| tri<ᵀ (□ A) (□ .A) | τ₌ A≮A′ refl A′≮A = τ₌ A′≮A refl A′≮A | |
| tri<ᵀ (□ A) (□ A′) | τ₎ A≮A′ A≢A′ A′<A = τ₎ A≮A′ (≢→□A≢□A′ A≢A′) A′<A | |
| tri<ᵀ (□ A) (A′ ∧ B′) = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (□ A) ⊤ = τ₍ ∙ (λ ()) I | |
| tri<ᵀ (A ∧ B) (α P′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (A ∧ B) (A′ ▻ B′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (A ∧ B) (□ A′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ (A ∧ B) (A′ ∧ B′) with tri<ᵀ A A′ | tri<ᵀ B B′ | |
| tri<ᵀ (A ∧ B) (A′ ∧ B′) | τ₍ A<A′ A≢A′ A′≮A | _ = τ₍ (ι₁ A<A′) (≢→A∧B≢A′∧B′ A≢A′) (≰→AB≮A′B′ {B = B′} A′≮A (sym≢ A≢A′)) | |
| tri<ᵀ (A ∧ B) (.A ∧ B′) | τ₌ A≮A′ refl A′≮A | τ₍ B<B′ B≢B′ B′≮B = τ₍ (ι₂ (refl , B<B′)) (≢→A∧B≢A∧B′ B≢B′) (≮→AB≮AB′ {B = B′} B′≮B) | |
| tri<ᵀ (A ∧ B) (.A ∧ .B) | τ₌ A≮A′ refl A′≮A | τ₌ B≮B′ refl B′≮B = τ₌ (irrefl<ᵀˣᵀ (A , B)) refl (irrefl<ᵀˣᵀ (A , B)) | |
| tri<ᵀ (A ∧ B) (.A ∧ B′) | τ₌ A≮A′ refl A′≮A | τ₎ B≮B′ B≢B′ B′<B = τ₎ (≮→AB≮AB′ {B = B} B≮B′) (≢→A∧B≢A∧B′ B≢B′) (ι₂ (refl , B′<B)) | |
| tri<ᵀ (A ∧ B) (A′ ∧ B′) | τ₎ A≮A′ A≢A′ A′<A | _ = τ₎ (≰→AB≮A′B′ {B = B} A≮A′ A≢A′) (≢→A∧B≢A′∧B′ A≢A′) (ι₁ A′<A) | |
| tri<ᵀ (A ∧ B) ⊤ = τ₍ ∙ (λ ()) I | |
| tri<ᵀ ⊤ (α P′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ ⊤ (A′ ▻ B′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ ⊤ (□ A′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ ⊤ (A′ ∧ B′) = τ₎ I (λ ()) ∙ | |
| tri<ᵀ ⊤ ⊤ = τ₌ I refl I |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment