-
Notifications
You must be signed in to change notification settings - Fork 1
/
Equiv2.agda
44 lines (34 loc) · 1.88 KB
/
Equiv2.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
{-# OPTIONS --without-K --exact-split --rewriting --overlapping-instances #-}
module Pi.Equiv.Equiv2 where
open import Pi.Syntax.Pi+.Indexed as Pi
open import Pi.Syntax.Pi^ as Pi^
open import Pi.UFin.UFin
open import Pi.Common.Extra
open import Pi.UFin.BAut
open import Pi.Equiv.Equiv0
open import Pi.Equiv.Equiv1
open import Pi.Equiv.Equiv2Norm
open import Pi.Equiv.Equiv2Hat
open import lib.Basics
open import lib.types.Fin
open import lib.types.List
open import lib.types.Truncation
open import lib.NType2
open import lib.types.SetQuotient
open import lib.types.Coproduct
private
variable
n m : ℕ
eval₂ : {t₁ t₂ : U n} {c₁ c₂ : t₁ ⟷₁ t₂} → c₁ ⟷₂ c₂ → eval₁ c₁ == eval₁ c₂
eval₂ = evalNorm₂ ∘ eval^₂
quote₂ : {t₁ t₂ : U n} {e₁ e₂ : Aut (Fin n)} (α : e₁ == e₂) → quote₁ {t₁ = t₁} {t₂ = t₂} idp e₁ ⟷₂ quote₁ {t₁ = t₁} {t₂ = t₂} idp e₂
quote₂ {n} {t₁ = t₁} {t₂ = t₂} {e₁ = e₁} {e₂ = e₂} α = transport (λ e → _⟷₂_ {n} {n} {t₁} {t₂} (quote₁ idp e₁) (quote₁ idp e)) α id⟷₂
-- NOTE: this is uip for ℕ
postulate
eq-size-idp-rewrite : {t₁ : U n} {t₂ : U n} {c : t₁ ⟷₁ t₂} → (⟷₁-eq-size c) ↦ idp
{-# REWRITE eq-size-idp-rewrite #-}
quote-eval₂ : {t₁ t₂ : U n} {c₁ c₂ : t₁ ⟷₁ t₂} (α : c₁ ⟷₂ c₂) → quote₂ (eval₂ α) ⟷₃ ((quote-eval₁ c₁) ■ ((id⟷₂ ⊡ (α ⊡ id⟷₂)) ■ (!⟷₂ (quote-eval₁ c₂))))
quote-eval₂ {c₁ = c₁} {c₂ = c₂} α = trunc _ _
eval-quote₂ : {e₁ e₂ : Aut (Fin n)} (α : e₁ == e₂) →
eval₂ {t₁ = quote₀ (pFin _)} {t₂ = quote₀ (pFin _)} (quote₂ α) == ap (λ e → (eval₁ (quote₁ {t₁ = quote₀ (pFin _)} {t₂ = quote₀ (pFin _)} idp e))) α
eval-quote₂ α = prop-has-all-paths {{has-level-apply (Aut-level {{Fin-is-set}}) _ _}} _ _