text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary using (Setoid)

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable

module SecondOrder.Term
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ

  -- The term judgement
  data Term (Θ : MContext) : ∀ (Γ : VContext) (A : sort) → Set ℓ

  Arg : ∀ (Θ : MContext) (Γ : VContext) (A : sort) (Δ : VContext) → Set ℓ
  Arg Θ Γ A Δ = Term Θ (Γ ,, Δ) A

  data Term Θ where
    tm-var : ∀ {Γ} {A} (x : A ∈ Γ) → Term Θ Γ A
    tm-meta : ∀ {Γᴹ A} {Γ} (M : [ Γᴹ , A ]∈ Θ)
                (ts : ∀ {B} (i : B ∈ Γᴹ) → Term Θ Γ B)
                → Term Θ Γ A
    tm-oper : ∀ {Γ} (f : oper) (es : ∀ (i : oper-arg f) → Arg Θ Γ (arg-sort f i) (arg-bind f i))
                → Term Θ Γ (oper-sort f)

  -- Syntactic equality of terms

  infix 4 _≈_

  data _≈_ {Θ : MContext} : ∀ {Γ : VContext} {A : sort} → Term Θ Γ A → Term Θ Γ A → Set ℓ where
    ≈-≡ : ∀ {Γ A} {t u : Term Θ Γ A} (ξ : t ≡ u) → t ≈ u
    ≈-meta : ∀ {Γ} {α A} {M : [ α , A ]∈ Θ} {ts us : ∀ {B} (i : B ∈ α) → Term Θ Γ B}
               (ξ : ∀ {B} i → ts {B} i ≈ us {B} i) → tm-meta M ts ≈ tm-meta M us
    ≈-oper : ∀ {Γ} {f : oper} {ds es : ∀ (i : oper-arg f) → Arg Θ Γ (arg-sort f i)  (arg-bind f i)}
               (ξ : ∀ i → ds i ≈ es i) → tm-oper f ds ≈ tm-oper f es

  -- Syntactic equality of terms is an equivalence relation

  ≈-refl : ∀ {Θ Γ A} {t : Term Θ Γ A} → t ≈ t
  ≈-refl = ≈-≡ refl

  ≈-sym : ∀ {Θ Γ A} {t u : Term Θ Γ A} → t ≈ u → u ≈ t
  ≈-sym (≈-≡ refl) = ≈-≡ refl
  ≈-sym (≈-meta ξ) = ≈-meta λ i → ≈-sym (ξ i)
  ≈-sym (≈-oper ξ) = ≈-oper (λ i → ≈-sym (ξ i))

  ≈-trans : ∀ {Θ Γ A} {t u v : Term Θ Γ A} → t ≈ u → u ≈ v → t ≈ v
  ≈-trans (≈-≡ refl) ξ = ξ
  ≈-trans (≈-meta ζ) (≈-≡ refl) = ≈-meta ζ
  ≈-trans (≈-meta ζ) (≈-meta ξ) = ≈-meta (λ i → ≈-trans (ζ i) (ξ i))
  ≈-trans (≈-oper ζ) (≈-≡ refl) = ≈-oper ζ
  ≈-trans (≈-oper ζ) (≈-oper ξ) = ≈-oper (λ i → ≈-trans (ζ i) (ξ i))

  Term-setoid : ∀ (Θ : MContext) (Γ : VContext)  (A : sort) → Setoid ℓ ℓ
  Term-setoid Θ Γ A =
    record
      { Carrier = Term Θ Γ A
      ; _≈_ = _≈_
      ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module Ix where

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> (I -> Set)
(S -:> T) i = S i -> T i
infixr 4 _-:>_

[_] : {I : Set} -> (I -> Set) -> Set
[ P ] = forall i -> P i

Algebra : {I : Set}(F : (I -> Set) -> (I -> Set)) -> (I -> Set) -> Set
Algebra F X = [ F X -:> X ]

ext: agda

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


text:
module AnonymousImport where

open import Common.IO as _
open import Common.Unit as _

main : IO Unit
main = putStrLn ""

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --without-K #-}
module Data.Fin.Relation.Binary.Closure where

open import Data.Fin
open import Data.Fin.Subset
open import Data.Fin.Subset.Dec
open import Data.Fin.Subset.Properties
open import Data.Fin.Subset.Properties.Dec
open import Data.Nat as ℕ using (ℕ)
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality as Eq
open import Relation.Binary renaming (Decidable to Dec₂)
open import Function using (flip; _∘_; case_of_; _∋_)
open import Data.List as List using (List; _∷_; [])
open import Data.Sum
import Data.List.Membership.Propositional as Mem
open import Data.List.Membership.Propositional.Properties as MemP
open import Data.Product
open import Induction.Nat
open import Data.Vec using (Vec; []; _∷_; here)
open import Data.Vec.Properties
open import Data.Bool.Properties as B
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Nat.Properties as ℕP
open import Function.Equivalence using (Equivalence)
open import Function.Equality using (_⟨$⟩_)

private
  iter : ∀ {a}{A : Set a} → (A → A) → A → ℕ → A
  iter f z ℕ.zero = z
  iter f z (ℕ.suc n) = f (iter f z n)
  _≟s_ : ∀ {n} → Dec₂ (_≡_{A = Subset n})
  _≟s_ = ≡-dec B._≟_
  p⊂q⇒∣p∣<∣q∣ : ∀ {n} {p q : Subset n} → p ⊆ q → p ≢ q → ∣ p ∣ ℕ.< ∣ q ∣
  p⊂q⇒∣p∣<∣q∣ {p = []} {[]} p⊆q p≢q = contradiction refl p≢q
  p⊂q⇒∣p∣<∣q∣ {p = outside ∷ p} {outside ∷ q} p⊆q p≢q = p⊂q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q) (p≢q ∘ cong (outside ∷_))
  p⊂q⇒∣p∣<∣q∣ {p = outside ∷ p} {inside ∷ q} p⊆q p≢q = ℕ.s≤s (p⊆q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q))
  p⊂q⇒∣p∣<∣q∣ {p = inside ∷ p} {outside ∷ q} p⊆q p≢q = contradiction (p⊆q here) λ ()
  p⊂q⇒∣p∣<∣q∣ {p = inside ∷ p} {inside ∷ q} p⊆q p≢q = ℕ.s≤s (p⊂q⇒∣p∣<∣q∣ (drop-∷-⊆ p⊆q) (p≢q ∘ cong (inside ∷_)))

  m<n⇒0<n : ∀ {m n} → m ℕ.< n → 0 ℕ.< n
  m<n⇒0<n (ℕ.s≤s m<n) = ℕ.s≤s ℕ.z≤n

  saturate : ∀ {n} → (f : Subset n → Subset n) → (∀ {s} → s ⊆ f s) → (z : Subset n) → iter f z n ≡ iter f z (ℕ.suc n)
  saturate {n} f p z = case rec P g n of
          λ { (inj₁ eq) → eq ;
               (inj₂ n<f) → contradiction n<f (≤⇒≯ (∣p∣≤n (f (iter f z n)))) }
    where
      open ℕP.≤-Reasoning
      P : ℕ → Set
      P n = iter f z n ≡ iter f z (ℕ.suc n) ⊎ n ℕ.< ∣ iter f z (ℕ.suc n) ∣

      g : ∀ n → Rec _ P n → P n
      g ℕ.zero _ with z ≟s f z
      ... | yes eq = inj₁ eq
      ... | no  z≢fz = inj₂ (m<n⇒0<n (p⊂q⇒∣p∣<∣q∣ p z≢fz))
      g (ℕ.suc n) (inj₁ eq) = inj₁ (cong f eq)
      g (ℕ.suc n) (inj₂ n<f) with f (iter f z n) ≟s f (iter f z (ℕ.suc n))
      ... | yes eq = inj₁ eq
      ... | no  neq = inj₂ (begin-strict ℕ.suc n <⟨ ℕ.s≤s n<f ⟩ _ ≤⟨ p⊂q⇒∣p∣<∣q∣ p neq ⟩ _ ∎)

  ∈-saturate : ∀ {n}(f : Subset n → Subset n)(p : ∀ {s} → s ⊆ f s) z {i} → (∃ λ m → i ∈ iter f z m) → i ∈ iter f z n
  ∈-saturate {n} f p z (m , i∈fm) with n ℕP.≤? m

  ... | yes n≤m rewrite sym (ℕP.m∸n+n≡m n≤m) = subst (_ ∈_) (sym (lemma (m ℕ.∸ n))) i∈fm
    where
      lemma : ∀ k → iter f z n ≡ iter f z (k ℕ.+ n)
      lemma 0 = refl
      lemma (ℕ.suc k) = trans (saturate f p z) (cong f (lemma k))

  ... | no n≰m  rewrite sym (ℕP.m∸n+n≡m (ℕP.≰⇒> n≰m)) = lemma (n ℕ.∸ ℕ.suc m) (p i∈fm)
    where
      lemma : ∀ k {m j} → j ∈ iter f z m → j ∈ iter f z (k ℕ.+ m)
      lemma 0 j∈fm = j∈fm
      lemma (ℕ.suc k) j∈fm = p (lemma k j∈fm)

module _ {n} where

  open import Data.List.Relation.Unary.Any

  ∈-⋃⁺ : ∀{s}{ss : List (Subset n)} → s Mem.∈ ss → ∀ {i} → i ∈ s → i ∈ ⋃ ss
  ∈-⋃⁺ {ss = []} () i∈s
  ∈-⋃⁺ {ss = s ∷ ss} (here refl) i∈s = x∈p∪q⁺ (inj₁ i∈s)
  ∈-⋃⁺ {ss = _ ∷ ss} (there s∈ss) i∈s = x∈p∪q⁺ (inj₂ (∈-⋃⁺ s∈ss i∈s))

  ∈-⋃⁻ : ∀{ss : List (Subset n)}{i} → i ∈ ⋃ ss → ∃ λ s → i ∈ s × s Mem.∈ ss
  ∈-⋃⁻ {[]} i∈ss = contradiction i∈ss ∉⊥
  ∈-⋃⁻ {s ∷ ss} i∈ss with x∈p∪q⁻ _ _ i∈ss
  ∈-⋃⁻ {s ∷ ss} i∈ss | inj₁ i∈s = s , i∈s , here refl
  ∈-⋃⁻ {_ ∷ ss} i∈ss | inj₂ i∈rest with ∈-⋃⁻ {ss} i∈rest
  ... | s , i∈s , s∈ss = s , i∈s , there s∈ss

module _ {p n}{P : Rel (Fin n) p} where
  right-image : Dec₂ P → Fin n → Subset n
  right-image P? i = subset (P? i)

  left-image  : Dec₂ P → Fin n → Subset n
  left-image P? i = subset (flip P? i)

  _◃_ : Subset n → Dec₂ P → Subset n
  s ◃ P? = ⋃ (List.map (right-image P?) (List.filter (_∈? s) (List.allFin _)))

  _▹_ :  Dec₂ P → Subset n → Subset n
  P? ▹ s = ⋃ (List.map (left-image P?) (List.filter (_∈? s) (List.allFin _)))

  _∪▹_ : Dec₂ P → Subset n →  Subset n
  P? ∪▹ s = s ∪ (P? ▹ s)

  ∪▹-monotone : (P? : Dec₂ P) → ∀ {s} → s ⊆ P? ∪▹ s
  ∪▹-monotone P? {s} = p⊆p∪q (P? ▹ s)

  ∈-▹⁺ : ∀ {i s j}(P? : Dec₂ P) → j ∈ s → P i j → i ∈ P? ▹ s
  ∈-▹⁺ {i}{s}{j} P? i∈s pij = ∈-⋃⁺ (∈-map⁺ (left-image P?) (∈-filter⁺ (_∈? s) (∈-allFin _) i∈s))  (∈subset⁺ (flip P? j) pij)

  ∈-▹⁻ : ∀ {i s}(P? : Dec₂ P) → i ∈ P? ▹ s → ∃ λ j → j ∈ s × P i j
  ∈-▹⁻ {i}{s} P? i∈s with ∈-⋃⁻ {ss = List.map (left-image P?) (List.filter (_∈? s) (List.allFin _))} i∈s
  ... | P▹s , i∈P▹s , P▹s∈ss with ∈-map⁻ _ P▹s∈ss
  ... | j , j∈l , eq rewrite eq with ∈-filter⁻  (_∈? s) {xs = List.allFin _} j∈l
  ... | _ , j∈s         = j ,  j∈s , ∈subset⁻ (flip P? j) i∈P▹s

  iter-∪▹ : Subset n → (P? : Dec₂ P) → ℕ → Subset n
  iter-∪▹ z P? = iter (P? ∪▹_) z

  ▹-star : (P? : Dec₂ P) → Fin n → ℕ → Subset n
  ▹-star P? i = iter-∪▹ ⁅ i ⁆ P?

  ▹-plus : (P? : Dec₂ P) → Fin n → ℕ → Subset n
  ▹-plus P? j = iter-∪▹ (left-image P? j) P?

  ∈-▹-star⁺ : (P? : Dec₂ P) → ∀ {i j} → Star P i j → i ∈ ▹-star P? j n
  ∈-▹-star⁺ P? {i}{j} pij = ∈-saturate _ (∪▹-monotone P?) ⁅ j ⁆ (rec Q g (length pij) pij refl)
    where
       length : ∀ {i j} → Star P i j → ℕ
       length ε = 0
       length (_ ◅ r) = 1 ℕ.+ length r

       Q : ℕ → Set _
       Q m = ∀ {i j} → (r : Star P i j) → length r ≡ m → ∃ λ k → i ∈ ▹-star P? j k

       g : ∀ m → Rec _ Q m → Q m
       g .0 ih ε refl = 0 , x∈⁅x⁆ _
       g .(ℕ.suc (length rkj)) ih (pik ◅ rkj) refl with ih rkj refl
       ... | k , i∈fk = 1 ℕ.+ k , x∈p∪q⁺ (inj₂ (∈-▹⁺ P? i∈fk pik))

  ∈-▹-star⁻ : (P? : Dec₂ P) → ∀ {i j} m → i ∈ ▹-star P? j m → Star P i j
  ∈-▹-star⁻ P? {i} {j} ℕ.zero h rewrite x∈⁅y⁆⇒x≡y _ h = ε
  ∈-▹-star⁻ P? {i} {j} (ℕ.suc m) h with x∈p∪q⁻ _ _ h
  ... | inj₁ h₁ = ∈-▹-star⁻ P? m h₁
  ... | inj₂ h₁  with ∈-▹⁻ P? h₁
  ... | k , k∈s , pik = pik ◅ ∈-▹-star⁻ P? m k∈s

  ∈-▹-plus⁺ : (P? : Dec₂ P) → ∀ {i j} → Plus′ P i j → i ∈ ▹-plus P? j n
  ∈-▹-plus⁺ P? {i}{j} pij = ∈-saturate _ (∪▹-monotone P?) (left-image P? j) (rec Q g (length pij) pij refl)
     where
       length : ∀ {i j} → Plus′ P i j → ℕ
       length [ x∼y ] = 0
       length (x∼y ∷ r) = 1 ℕ.+ length r

       Q : ℕ → Set _
       Q m = ∀ {i j} → (r : Plus′ P i j) → length r ≡ m → ∃ λ k → i ∈ ▹-plus P? j k

       g : ∀ m → Rec _ Q m → Q m
       g ℕ.zero ih {i}{j} [ pij ] refl = 0 , ∈subset⁺ (flip P? j) pij
       g (ℕ.suc .(length r)) ih {i}{j} (pik ∷ r) refl with ih r refl
       ... | k , i∈fk = 1 ℕ.+ k , x∈p∪q⁺ (inj₂ (∈-▹⁺ P? i∈fk pik))

  ∈-▹-plus⁻ : (P? : Dec₂ P) → ∀ {i j} m → i ∈ ▹-plus P? j m → Plus′ P i j
  ∈-▹-plus⁻ P? {i} {j} ℕ.zero h = [ ∈subset⁻ (flip P? j) h ]
  ∈-▹-plus⁻ P? {i} {j} (ℕ.suc m) h with x∈p∪q⁻ _ _ h
  ∈-▹-plus⁻ P? {i} {j} (ℕ.suc m) h | inj₁ h₁  = ∈-▹-plus⁻ P? m h₁
  ∈-▹-plus⁻ P? {i} {j} (ℕ.suc m) h | inj₂ h₁  with ∈-▹⁻ P? h₁
  ... | k , k∈s , pik = pik ∷ ∈-▹-plus⁻ P? m k∈s

  -- Derived decidability of closures

  dec-Star : (P? : Dec₂ P) → Dec₂ (Star P)
  dec-Star P? i j with i ∈? ▹-star P? j n
  ... | yes i∈star = yes (∈-▹-star⁻ P? n i∈star)
  ... | no i∉star  = no λ h → contradiction (∈-▹-star⁺ P? h) i∉star

  dec-Plus′ : (P? : Dec₂ P) → Dec₂ (Plus′ P)
  dec-Plus′ P? i j with i ∈? ▹-plus P? j n
  ... | yes i∈plus = yes (∈-▹-plus⁻ P? n i∈plus)
  ... | no i∉plus  = no λ h → contradiction (∈-▹-plus⁺ P? h) i∉plus

  dec-Plus : (P? : Dec₂ P) → Dec₂ (Plus P)
  dec-Plus P? i j with dec-Plus′ P? i j
  ... | yes pij′ = yes (Equivalence.from equivalent ⟨$⟩ pij′)
  ... | no ¬pij′ = no λ pij → ¬pij′ (Equivalence.to equivalent ⟨$⟩ pij)

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
{-# OPTIONS --cubical --safe #-}

module Data.Binary.Order where

open import Prelude
open import Data.Binary.Definition
open import Data.Bits.Order.Reverse public

-- weaken : ∀ xs ys → T (xs ≲ᴮ ys & false) → T (xs ≲ᴮ ys & true)
-- weaken 0ᵇ ys xs≲ys = tt
-- weaken (1ᵇ x) 0ᵇ xs≲ys = xs≲ys
-- weaken (1ᵇ x) (1ᵇ x₁) xs≲ys = weaken x x₁ xs≲ys
-- weaken (1ᵇ x) (2ᵇ x₁) xs≲ys = xs≲ys
-- weaken (2ᵇ x) 0ᵇ xs≲ys = xs≲ys
-- weaken (2ᵇ x) (1ᵇ x₁) xs≲ys = xs≲ys
-- weaken (2ᵇ x) (2ᵇ x₁) xs≲ys = weaken x x₁ xs≲ys

-- ≲-trans : ∀ sₒ xs ys zs s₁ s₂ → T (xs ≲ᴮ ys & s₁) → T (ys ≲ᴮ zs & s₂) → T (xs ≲ᴮ zs & (sₒ or s₁ and s₂))
-- ≲-trans true 0ᵇ       ys zs s₁ s₂ xs≲ys ys≲zs = tt
-- ≲-trans true (1ᵇ xs) (1ᵇ ys) (1ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs s₁    s₂    xs≲ys ys≲zs
-- ≲-trans true (1ᵇ xs) (1ᵇ ys) (2ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs s₁    true  xs≲ys ys≲zs
-- ≲-trans true (1ᵇ xs) (2ᵇ ys) (1ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs true  false xs≲ys ys≲zs
-- ≲-trans true (1ᵇ xs) (2ᵇ ys) (2ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs true  s₂    xs≲ys ys≲zs
-- ≲-trans true (2ᵇ xs) (1ᵇ ys) (1ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false s₂    xs≲ys ys≲zs
-- ≲-trans true (2ᵇ xs) (1ᵇ ys) (2ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs false true  xs≲ys ys≲zs
-- ≲-trans true (2ᵇ xs) (2ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false false xs≲ys ys≲zs
-- ≲-trans true (2ᵇ xs) (2ᵇ ys) (1ᵇ zs) true  s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs true  false xs≲ys ys≲zs
-- ≲-trans true (2ᵇ xs) (2ᵇ ys) (2ᵇ zs) s₁    s₂ xs≲ys ys≲zs = ≲-trans true  xs ys zs s₁    s₂    xs≲ys ys≲zs
-- ≲-trans false 0ᵇ (1ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (1ᵇ ys) (2ᵇ zs) false s₂ xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (2ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (2ᵇ ys) (2ᵇ zs) false s₂ xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ 0ᵇ zs true false xs≲ys ys≲zs = ys≲zs
-- ≲-trans false 0ᵇ (1ᵇ ys) (1ᵇ zs) true false xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (1ᵇ ys) (2ᵇ zs) true false xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (2ᵇ ys) (1ᵇ zs) true false xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ (2ᵇ ys) (2ᵇ zs) true false xs≲ys ys≲zs = tt
-- ≲-trans false 0ᵇ ys zs true true xs≲ys ys≲zs = tt
-- ≲-trans false (1ᵇ xs) (1ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false s₂ xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (1ᵇ ys) (2ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans true xs ys zs false true xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (2ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs true false xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (2ᵇ ys) (2ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans true xs ys zs true s₂ xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (1ᵇ ys) (1ᵇ zs) true s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs true s₂ xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (1ᵇ ys) (2ᵇ zs) true s₂ xs≲ys ys≲zs = ≲-trans true xs ys zs true true xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (2ᵇ ys) (1ᵇ zs) true false xs≲ys ys≲zs = ≲-trans false xs ys zs true false xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (2ᵇ ys) (1ᵇ zs) true true xs≲ys ys≲zs = ≲-trans true xs ys zs true false xs≲ys ys≲zs
-- ≲-trans false (1ᵇ xs) (2ᵇ ys) (2ᵇ zs) true s₂ xs≲ys ys≲zs = ≲-trans true xs ys zs true s₂ xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (1ᵇ ys) (1ᵇ zs) s₁ s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false s₂ xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (1ᵇ ys) (2ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false true xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (1ᵇ ys) (2ᵇ zs) true false xs≲ys ys≲zs = ≲-trans false xs ys zs false true xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (1ᵇ ys) (2ᵇ zs) true true xs≲ys ys≲zs = ≲-trans true xs ys zs false true xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (2ᵇ ys) (1ᵇ zs) false s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs false false xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (2ᵇ ys) (1ᵇ zs) true s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs true false xs≲ys ys≲zs
-- ≲-trans false (2ᵇ xs) (2ᵇ ys) (2ᵇ zs) s₁ s₂ xs≲ys ys≲zs = ≲-trans false xs ys zs s₁ s₂ xs≲ys ys≲zs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems of ¬ connective.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Negation ( n : ℕ ) where

------------------------------------------------------------------------------

open import Data.PropFormula.Properties n using ( ¬-injective ; subst )
open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems.Classical n
open import Data.PropFormula.Theorems.Implication n using ( subst⊢⊃₁ )

open import Function using ( _$_ ; _∘_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym )

------------------------------------------------------------------------------

-- Theorem.
¬-equiv₁
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ φ
  → Γ ⊢ φ ⊃ ⊥
¬-to-⊃⊥ = ¬-equiv₁

-- Proof.
¬-equiv₁ {φ = φ} Γ⊢¬φ =
  ⊃-intro
    (¬-elim
      (weaken φ Γ⊢¬φ)
      (assume φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬-equiv₂
  : ∀ {Γ} {φ}
  → Γ ⊢ φ ⊃ ⊥
  → Γ ⊢ ¬ φ
⊃⊥-to-¬ = ¬-equiv₂

-- Proof.
¬-equiv₂ {φ = φ} Γ⊢φ⊃⊥ =
  ¬-intro
    (⊃-elim
      (weaken φ Γ⊢φ⊃⊥)
      (assume φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬¬-equiv₁
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ (¬ φ)
  → Γ ⊢ φ

-- Proof.
¬¬-equiv₁ {Γ}{φ} Γ⊢¬¬φ =
  (⊃-elim
    (⊃-intro $ RAA
      (¬-elim
        (weaken (¬ φ) $
          assume $ ¬ (¬ φ))
        (assume {Γ = Γ , ¬ (¬ φ)} $ ¬ φ)))
    Γ⊢¬¬φ)
-------------------------------------------------------------------------- ∎

-- Theorem.
¬¬-equiv₂
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ ¬ (¬ φ)

-- Proof.
¬¬-equiv₂ {Γ}{φ} Γ⊢φ =
  ⊃⊥-to-¬
    (⊃-intro
      (¬-elim
        (assume (¬ φ))
        (weaken (¬ φ) Γ⊢φ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬∨-to-⊃
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ∨ ψ
  → Γ ⊢ φ ⊃ ψ

-- Proof.
¬∨-to-⊃ {Γ}{φ}{ψ} =
  ⊃-elim $
    ⊃-intro $
      ∨-elim
        (⊃-intro $
          ⊥-elim {Γ = Γ , ¬ φ , φ} ψ
          (¬-elim
            (weaken φ $
              assume (¬ φ))
            (assume {Γ = Γ , ¬ φ} φ)))
        (⊃-intro $
          weaken φ $
            assume ψ)
-------------------------------------------------------------------------- ∎

-- Theorem.
¬⊤-to-⊥
  : ∀ {Γ}
  → Γ ⊢ ¬ ⊤
  → Γ ⊢ ⊥

-- Proof.
¬⊤-to-⊥ Γ⊢¬⊤ = ¬-elim Γ⊢¬⊤ ⊤-intro
-------------------------------------------------------------------------- ∎

-- Theorem.
⊤-to-¬⊥
  : ∀ {Γ}
  → Γ ⊢ ⊤
  → Γ ⊢ ¬ ⊥

-- Proof.
⊤-to-¬⊥ = λ _ → ¬-intro (assume ⊥)
-------------------------------------------------------------------------- ∎

-- Theorem.
¬⊥-to-⊤
  : ∀ {Γ}
  → Γ ⊢ ¬ ⊥
  → Γ ⊢ ⊤

-- Proof.
¬⊥-to-⊤ Γ⊢¬⊥ = ⊤-intro
-------------------------------------------------------------------------- ∎

-- Theorem.
⊥-to-¬⊤
  : ∀ {Γ}
  → Γ ⊢ ⊥
  → Γ ⊢ ¬ ⊤

-- Proof.
⊥-to-¬⊤ = ¬-intro ∘ weaken ⊤
-------------------------------------------------------------------------- ∎

-- Theorem.
¬-inside
  : ∀ {Γ} {φ ψ}
  → φ ≡ ψ
  → Γ ⊢ ¬ φ
  → Γ ⊢ ¬ ψ
≡-¬-to-¬ = ¬-inside

-- Proof.
¬-inside {φ = φ}{ψ} φ≡ψ Γ⊢¬φ =
  ¬-equiv₂
    (⊃-intro
      (⊃-elim
        (¬-equiv₁
          (weaken ψ Γ⊢¬φ))
        (subst
          (sym φ≡ψ)
          (assume ψ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢¬
  : ∀ {Γ} {φ γ}
  → Γ ⊢ γ ⊃ φ
  → Γ ⊢ ¬ φ
  → Γ ⊢ ¬ γ

-- Proof.
subst⊢¬ Γ⊢γ⊃φ Γ⊢¬φ = ⊃⊥-to-¬ (subst⊢⊃₁ Γ⊢γ⊃φ (¬-to-⊃⊥ Γ⊢¬φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬⇔-to-⊃¬∧⊃¬
  : ∀ {Γ} {φ₁ φ₂}
  → Γ ⊢ ¬ (φ₁ ⇔ φ₂)
  → Γ ⊢ (φ₁ ⊃ ¬ φ₂) ∧ (φ₂ ⊃ ¬ φ₁)

-- Proof.
¬⇔-to-⊃¬∧⊃¬ {Γ}{φ₁}{φ₂} thm =
  ∧-intro
    (⊃-intro
      (¬-intro
        (¬-elim
          (weaken φ₂ $ weaken φ₁ thm)
          (⇔-intro
            (weaken φ₁ $ assume {Γ = Γ , φ₁} φ₂)
            (weaken φ₂ $ weaken φ₂ $ assume φ₁)))))
    (⊃-intro
      (¬-intro
        (¬-elim (weaken φ₁ $ weaken φ₂ thm)
          (⇔-intro
            (weaken φ₁ $ weaken φ₁ $ assume φ₂)
            (weaken φ₂ $ assume {Γ = Γ , φ₂} φ₁)))))
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category

-- Lifting Properties
module Categories.Morphism.Lifts {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open Category 𝒞
open Definitions 𝒞

-- A pair of morphisms has the lifting property if every commutative
-- square admits a diagonal filler. We say that 'i' has the left lifting
-- property with respect to 'p', and that 'p' has the right lifting property
-- with respect to 'i'.
--
-- Graphically, the situation is as follows:
--
--      f
--   A ────> X
--   │     ^ │
--   │  ∃ ╱  │
-- i │   ╱   │ p
--   │  ╱    │
--   V ╱     V
--   B ────> Y
--      g
--
-- Note that the filler is /not/ required to be unique.
--
-- For ease of use, we define lifts in two steps:
-- * 'Filler' describes the data required to fill a /particular/ commutative square.
-- * 'Lifts' then quantifies over all commutative squares.

record Filler {A B X Y} {i : A ⇒ B} {f : A ⇒ X} {g : B ⇒ Y} {p : X ⇒ Y}
              (comm : CommutativeSquare i f g p) : Set (ℓ ⊔ e) where
  field
    filler : B ⇒ X
    fill-commˡ : filler ∘ i ≈ f
    fill-commʳ : p ∘ filler ≈ g

Lifts : ∀ {A B X Y} → (i : A ⇒ B) → (p : X ⇒ Y) → Set (ℓ ⊔ e)
Lifts i p = ∀ {f g} → (comm : CommutativeSquare i f g p) → Filler comm

--------------------------------------------------------------------------------
-- Lifings of Morphism Classes

-- Shorthand for denoting a class of morphisms.
MorphismClass : (p : Level) → Set (o ⊔ ℓ ⊔ suc p)
MorphismClass p = ∀ {X Y} → X ⇒ Y → Set p

-- A morphism 'i' is called "projective" with respect to some morphism class 'J'
-- if it has the left-lifting property against every element of 'J'.
Projective : ∀ {j} {A B} → MorphismClass j → (i : A ⇒ B) → Set (o ⊔ ℓ ⊔ e ⊔ j)
Projective J i = ∀ {X Y} → (f : X ⇒ Y) → J f → Lifts i f

-- Dually, a morphism 'i' is called "injective" with repsect to a morphism class 'J'
-- if it has the right-lifting property against every element of 'J'.
Injective : ∀ {j} {A B} → MorphismClass j → (i : A ⇒ B) → Set (o ⊔ ℓ ⊔ e ⊔ j)
Injective J i = ∀ {X Y} → (f : X ⇒ Y) → J f → Lifts f i

-- The class of J-Projective morphisms.
Proj : ∀ {j} (J : MorphismClass j) → MorphismClass (o ⊔ ℓ ⊔ e ⊔ j)
Proj J = Projective J

-- The class of J-Injective morphisms.
Inj : ∀ {j} (J : MorphismClass j) → MorphismClass (o ⊔ ℓ ⊔ e ⊔ j)
Inj J = Injective J

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Data.Nat    using (ℕ; _+_; _≤?_)
open import Data.Bool   using (Bool; true; false; not; _∧_)
open import Data.String using (String; _≟_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
open import Function.Equivalence using (_⇔_; equivalence)

open import IMP

data ⦅_,_⦆⇒_ : com → state → state → Set where
  Skip : ∀{s} → ⦅ SKIP , s ⦆⇒ s
  Loc : ∀{x a s}
      → ⦅ x ::= a , s ⦆⇒ (s [ x ::= aval a s ])
  Comp : ∀{c₁ c₂ s₁ s₂ s₃}
       → ⦅ c₁ , s₁ ⦆⇒ s₂
       → ⦅ c₂ , s₂ ⦆⇒ s₃
       → ⦅ c₁ :: c₂ , s₁ ⦆⇒ s₃
  IfTrue : ∀{c₁ c₂ b s t}
         → bval b s ≡ true
         → ⦅ c₁ , s ⦆⇒ t
         → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆⇒ t
  IfFalse : ∀{c₁ c₂ b s t}
          → bval b s ≡ false
          → ⦅ c₂ , s ⦆⇒ t
          → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆⇒ t
  WhileFalse : ∀{c b s}
             → bval b s ≡ false
             → ⦅ WHILE b DO c , s ⦆⇒ s
  WhileTrue  : ∀{c b s₁ s₂ s₃}
             → bval b s₁ ≡ true
             → ⦅ c , s₁ ⦆⇒ s₂
             → ⦅ WHILE b DO c , s₂ ⦆⇒ s₃
             → ⦅ WHILE b DO c , s₁ ⦆⇒ s₃

true≢false : ¬ (true ≡ false)
true≢false = λ ()

deterministic : ∀{c s t t′}
              → ⦅ c , s ⦆⇒ t
              → ⦅ c , s ⦆⇒ t′
              → t ≡ t′
deterministic Skip Skip = refl
deterministic Loc Loc = refl
deterministic (Comp r₁ r₂)  (Comp r₁′ r₂′) rewrite deterministic r₁ r₁′ = deterministic r₂ r₂′
deterministic (IfTrue v r)  (IfTrue  v′ r′) = deterministic r r′
deterministic (IfTrue v r)  (IfFalse v′ r′) rewrite v  = contradiction v′ true≢false
deterministic (IfFalse v r) (IfTrue  v′ r′) rewrite v′ = contradiction v true≢false
deterministic (IfFalse v r) (IfFalse v′ r′) = deterministic r r′
deterministic (WhileFalse v) (WhileFalse x₁) = refl
deterministic (WhileFalse v) (WhileTrue x₁ r₁ r₂) rewrite x₁ = contradiction v  true≢false
deterministic (WhileTrue v r₁ r₂) (WhileFalse v′) rewrite v  = contradiction v′ true≢false
deterministic (WhileTrue v r₁ r₂) (WhileTrue v′ r₁′ r₂′) rewrite deterministic r₁ r₁′ = deterministic r₂ r₂′

lemma2-3-5 : ∀{s t}
           → ¬ ( ⦅ WHILE (Bc true) DO SKIP , s ⦆⇒ t )
lemma2-3-5 (WhileTrue x Skip (WhileTrue v r₁ r₂)) = lemma2-3-5 r₂

infixl 19 _∼_
_∼_ : com → com → Set
c ∼ c′ = ∀{s t} → ⦅ c , s  ⦆⇒ t ⇔ ⦅ c′ , s ⦆⇒ t

lemma2-4-3 : ∀{b c} → (WHILE b DO c) ∼ (IF b THEN (c :: (WHILE b DO c)) ELSE SKIP)
lemma2-4-3 = equivalence (λ { (WhileFalse x) → IfFalse x Skip ; (WhileTrue x r r₁) → IfTrue x (Comp r r₁) })
                         (λ { (IfTrue x (Comp r r₁)) → WhileTrue x r r₁ ; (IfFalse x Skip) → WhileFalse x })

data ⦅_,_⦆→⦅_,_⦆ : com → state → com → state → Set where
  Loc : ∀{x a s}
      → ⦅ x ::= a , s ⦆→⦅ SKIP , s [ x ::= aval a s ] ⦆
  Comp₁ : ∀{c s}
        → ⦅ SKIP :: c , s ⦆→⦅ c , s ⦆
  Comp₂ : ∀{c₁ c₁′ c₂ s s′}
        → ⦅ c₁       , s ⦆→⦅ c₁′       , s′ ⦆
        → ⦅ c₁ :: c₂ , s ⦆→⦅ c₁′ :: c₂ , s′ ⦆
  IfTrue  : ∀{b s c₁ c₂}
          → bval b s ≡ true
          → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⦅ c₁ , s ⦆
  IfFalse : ∀{b s c₁ c₂}
          → bval b s ≡ false
          → ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⦅ c₂ , s ⦆
  While : ∀{b s c}
        → ⦅ WHILE b DO c , s ⦆→⦅ IF b THEN (c :: (WHILE b DO c)) ELSE SKIP , s ⦆

infix  3 ⦅_,_⦆∎
infixr 2 ⦅_,_⦆→⟨_⟩_ ⦅_,_⦆→*⟨_⟩_

data  ⦅_,_⦆→*⦅_,_⦆ : com → state → com → state → Set where
  ⦅_,_⦆∎ : ∀ c s → ⦅ c , s ⦆→*⦅ c , s ⦆
  ⦅_,_⦆→⟨_⟩_ : ∀ c s {c′ c″ s′ s″}
            → ⦅ c  , s  ⦆→⦅  c′ , s′ ⦆
            → ⦅ c′ , s′ ⦆→*⦅ c″ , s″ ⦆
            → ⦅ c  , s  ⦆→*⦅ c″ , s″ ⦆

⦅_,_⦆→*⟨_⟩_ : ∀ c s {c′ c″ s′ s″}
           → ⦅ c  , s  ⦆→*⦅ c′ , s′ ⦆
           → ⦅ c′ , s′ ⦆→*⦅ c″ , s″ ⦆
           → ⦅ c  , s  ⦆→*⦅ c″ , s″ ⦆
⦅ c , s ⦆→*⟨ ⦅ _ , _ ⦆∎ ⟩        b = b
⦅ c , s ⦆→*⟨ ⦅ _ , _ ⦆→⟨ x ⟩ r ⟩ b = ⦅ _ , _ ⦆→⟨ x ⟩ ⦅ _ , _ ⦆→*⟨ r ⟩ b

lemma2-5-6 : ∀{c₁ c₁′ c₂ s s′}
      → ⦅ c₁ , s       ⦆→*⦅ c₁′       ,  s′ ⦆
      → ⦅ c₁ :: c₂ , s ⦆→*⦅ c₁′ :: c₂ ,  s′ ⦆
lemma2-5-6  ⦅ _ , _ ⦆∎         = ⦅ _ , _ ⦆∎
lemma2-5-6 (⦅ _ , _ ⦆→⟨ x ⟩ r) = ⦅ _ , _ ⦆→⟨ Comp₂ x ⟩ lemma2-5-6 r

big-small : ∀{c s t}
          → ⦅ c , s ⦆⇒ t
          → ⦅ c , s ⦆→*⦅ SKIP , t ⦆
big-small (Skip {s}) =
  ⦅ SKIP , s ⦆∎
big-small (Loc {x}{s}{a}) =
  ⦅ x ::= s , a                    ⦆→⟨ Loc ⟩
  ⦅ SKIP    , a [ x ::= aval s a ] ⦆∎
big-small (Comp {c₁}{c₂}{s}{s′}{t} r₁ r₂) =
  ⦅ c₁   :: c₂ , s  ⦆→*⟨ lemma2-5-6 (big-small r₁) ⟩
  ⦅ SKIP :: c₂ , s′ ⦆→⟨  Comp₁ ⟩
  ⦅ c₂         , s′ ⦆→*⟨ big-small r₂ ⟩
  ⦅ SKIP       , t  ⦆∎
big-small (IfTrue {c₁}{c₂}{b}{s}{t} v r₁) =
  ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⟨ IfTrue v ⟩
  ⦅ c₁                   , s ⦆→*⟨ big-small r₁ ⟩
  ⦅ SKIP                 , t ⦆∎
big-small (IfFalse {c₁}{c₂}{b}{s}{t} v r₂) =
  ⦅ IF b THEN c₁ ELSE c₂ , s ⦆→⟨ IfFalse v ⟩
  ⦅ c₂                   , s ⦆→*⟨ big-small r₂ ⟩
  ⦅ SKIP                 , t ⦆∎
big-small (WhileFalse {c}{b}{s} v) =
  ⦅ WHILE b DO c                            , s ⦆→⟨ While ⟩
  ⦅ IF b THEN c :: (WHILE b DO c) ELSE SKIP , s ⦆→⟨ IfFalse v ⟩
  ⦅ SKIP                                    , s ⦆∎
big-small (WhileTrue {c}{b}{s}{s′}{t} v r₁ r₂) =
  ⦅ WHILE b DO c                            , s  ⦆→⟨ While ⟩
  ⦅ IF b THEN c :: (WHILE b DO c) ELSE SKIP , s  ⦆→⟨ IfTrue v ⟩
  ⦅ c :: (WHILE b DO c)                     , s  ⦆→*⟨ lemma2-5-6 (big-small r₁) ⟩
  ⦅ SKIP :: (WHILE b DO c)                  , s′ ⦆→⟨ Comp₁ ⟩
  ⦅ WHILE b DO c                            , s′ ⦆→*⟨ big-small r₂ ⟩
  ⦅ SKIP                                    , t  ⦆∎

lemma2-5-8 : ∀{c s c′ s′ t}
           → ⦅ c  , s  ⦆→⦅ c′ , s′ ⦆ → ⦅ c′ , s′ ⦆⇒ t
           → ⦅ c  , s  ⦆⇒ t
lemma2-5-8 Loc Skip = Loc
lemma2-5-8 Comp₁ r₁ = Comp Skip r₁
lemma2-5-8 (Comp₂ x) (Comp r₁ r₂) = Comp (lemma2-5-8 x r₁) r₂
lemma2-5-8 (IfTrue x) r₁ = IfTrue x r₁
lemma2-5-8 (IfFalse x) r₁ = IfFalse x r₁
lemma2-5-8 While (IfTrue x (Comp r₁ r₂)) = WhileTrue x r₁ r₂
lemma2-5-8 While (IfFalse x Skip) = WhileFalse x

small-big : ∀{c s t}
          → ⦅ c , s ⦆→*⦅ SKIP , t ⦆
          → ⦅ c , s ⦆⇒ t
small-big ⦅ SKIP , s ⦆∎ = Skip
small-big (⦅ c , s ⦆→⟨ x ⟩ r) = lemma2-5-8 x (small-big r)

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
module Oscar.Data.Term.AlphaConversion {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Term FunctionName

open import Oscar.Class.AlphaConversion
open import Oscar.Data.Equality
open import Oscar.Data.Fin
open import Oscar.Data.Vec
open import Oscar.Function
open import Oscar.Relation

import Oscar.Data.Term.AlphaConversion.internal FunctionName as ⋆

instance AlphaConversionFinTerm : AlphaConversion Fin Term
AlphaConversion._◂_ AlphaConversionFinTerm = ⋆._◂_
AlphaConversion.◂-identity AlphaConversionFinTerm = ⋆.◂-identity
AlphaConversion.◂-associativity AlphaConversionFinTerm = ⋆.◂-associativity
AlphaConversion.◂-extensionality AlphaConversionFinTerm = ⋆.◂-extensionality

instance AlphaConversionFinTerms : ∀ {N} → AlphaConversion Fin (Terms N)
AlphaConversion._◂_ AlphaConversionFinTerms _ = ⋆._◂s_ _
AlphaConversion.◂-identity AlphaConversionFinTerms = ⋆.◂s-identity
AlphaConversion.◂-associativity AlphaConversionFinTerms _ _ = ⋆.◂s-associativity _ _
AlphaConversion.◂-extensionality AlphaConversionFinTerms f≡̇g = ⋆.◂s-extensionality f≡̇g


text:
postulate A : Set
variable  a : A

postulate B : A → Set
variable  b : B a

postulate C : B a → Set
variable  c : C b

postulate
  _==_  : {b b' : B a} → C b → C b' → Set
  _=='_ : {b : B a} → C b → C b → Set

postulate
  f : (b : B a) (b' : B {!a!}) → Set
  g : (c : C b) (c' : C {!b!}) → c == c' → Set

module _ (X : Set) where
  postulate
    h : (b' : B a) (c : C b) (c' : C b') → {!c'!} ==' c' → Set


text:
{- Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Bool where

open import B.Prelude.BooleanAlgebra using (BooleanAlgebra)
import Data.Bool
import Data.Bool.Properties

open Data.Bool
  using (Bool; if_then_else_; T)
  public

instance
  BooleanAlgebra-Bool : BooleanAlgebra _ _
  BooleanAlgebra-Bool = Data.Bool.Properties.booleanAlgebra

module Bool where
  open Data.Bool
    using (_xor_)
    public

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import homotopy.Bouquet
open import homotopy.SphereEndomorphism
open import groups.SphereEndomorphism
open import groups.CoefficientExtensionality
open import cw.CW
open import cw.FinCW
open import cw.WedgeOfCells
open import cw.DegreeByProjection {lzero}

module cw.FinBoundary where

  fdegree-last : ∀ {n} (fin-skel : FinSkeleton (S n))
    → cells-last (FinSkeleton-realize fin-skel)
    → cells-last (cw-init (FinSkeleton-realize fin-skel)) → ℤ
  fdegree-last fin-skel = degree-last (FinSkeleton-realize fin-skel) (FinSkeleton-has-cells-with-dec-eq fin-skel)

  fdegree-nth : ∀ {m n} (Sm≤n : S m ≤ n) (fin-skel : FinSkeleton n)
    → cells-nth Sm≤n (FinSkeleton-realize fin-skel)
    → cells-last (cw-init (cw-take Sm≤n (FinSkeleton-realize fin-skel))) → ℤ
  fdegree-nth Sm≤n fin-skel = degree-nth Sm≤n (FinSkeleton-realize fin-skel) (FinSkeleton-has-cells-with-dec-eq fin-skel)

  FinSkeleton-has-degrees-with-finite-support : ∀ {n} (fin-skel : FinSkeleton n)
    → has-degrees-with-finite-support
        (FinSkeleton-realize fin-skel)
        (FinSkeleton-has-cells-with-dec-eq fin-skel)
  FinSkeleton-has-degrees-with-finite-support {n = O} _ = _
  FinSkeleton-has-degrees-with-finite-support {n = S O} _ = _ , (λ _ → Fin→-has-finite-support _)
  FinSkeleton-has-degrees-with-finite-support {n = S (S n)} (attached-fin-skeleton skel _ _) =
    FinSkeleton-has-degrees-with-finite-support {n = S n} skel , (λ _ → Fin→-has-finite-support _)

  fboundary'-last : ∀ {n} (fin-skel : FinSkeleton (S n))
    → cells-last (FinSkeleton-realize fin-skel)
    → FreeAbGroup.El (cells-last (cw-init (FinSkeleton-realize fin-skel)))
  fboundary'-last fin-skel upper = boundary'-last
    (FinSkeleton-realize fin-skel)
    (FinSkeleton-has-cells-with-dec-eq fin-skel)
    (FinSkeleton-has-degrees-with-finite-support fin-skel)
    upper

  fboundary-last : ∀ {n} (fin-skel : FinSkeleton (S n))
    →  FreeAbGroup.grp (cells-last (FinSkeleton-realize fin-skel))
    →ᴳ FreeAbGroup.grp (cells-last (cw-init (FinSkeleton-realize fin-skel)))
  fboundary-last fin-skel = FreeAbGroup-extend
    (FreeAbGroup (cells-last (cw-init (FinSkeleton-realize fin-skel))))
    (fboundary'-last fin-skel)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 17-groups where

import 16-sets
open 16-sets public

-- Section 12.3 Groups in univalent mathematics

{- We first introduce semi-groups, and then groups. We do this because the
   category of groups is a full subcategory of the category of semi-groups.
   In particular, it is a proposition for a semi-group to be a group. Therefore
   this approach gives us in a straightforward way that equality of groups is
   equality of semi-groups. This will be useful in showing that group
   isomorphisms are equivalent to identifications of groups. -}

has-associative-mul :
  {l : Level} (X : UU-Set l) → UU l
has-associative-mul X =
  Σ ( ( type-Set X) →
      ( ( type-Set X) → (type-Set X))) (λ μ →
    ( x y z : type-Set X) → Id (μ (μ x y) z) (μ x (μ y z)))

Semi-Group :
  (l : Level) → UU (lsuc l)
Semi-Group l = Σ (UU-Set l) has-associative-mul

{- Bureaucracy of semi-groups. -}

set-Semi-Group :
  {l : Level} → Semi-Group l → UU-Set l
set-Semi-Group G = pr1 G

type-Semi-Group :
  {l : Level} → Semi-Group l → UU l
type-Semi-Group G = pr1 (set-Semi-Group G)

is-set-type-Semi-Group :
  {l : Level} (G : Semi-Group l) → is-set (type-Semi-Group G)
is-set-type-Semi-Group G = pr2 (set-Semi-Group G)

associative-mul-Semi-Group :
  {l : Level} (G : Semi-Group l) →
  has-associative-mul (set-Semi-Group G)
associative-mul-Semi-Group G = pr2 G

mul-Semi-Group :
  {l : Level} (G : Semi-Group l) →
  type-Semi-Group G →
    type-Semi-Group G → type-Semi-Group G
mul-Semi-Group G = pr1 (associative-mul-Semi-Group G)

is-associative-mul-Semi-Group :
  {l : Level} (G : Semi-Group l) (x y z : type-Semi-Group G) →
  Id ( mul-Semi-Group G (mul-Semi-Group G x y) z)
     ( mul-Semi-Group G x (mul-Semi-Group G y z))
is-associative-mul-Semi-Group G = pr2 (associative-mul-Semi-Group G)

{- The property that a semi-group is a monoid is just that the semi-group
   possesses a unit that satisfies the left and right unit laws. -}

is-unital :
  {l : Level} → Semi-Group l → UU l
is-unital G =
  Σ ( type-Semi-Group G)
    ( λ e →
      ( (y : type-Semi-Group G) → Id (mul-Semi-Group G e y) y) ×
      ( (x : type-Semi-Group G) → Id (mul-Semi-Group G x e) x))

{- We show that is-unital is a proposition. -}

abstract
  is-prop-is-unital' :
    {l : Level} (G : Semi-Group l) → is-prop' (is-unital G)
  is-prop-is-unital' (pair (pair X is-set-X) (pair μ assoc-μ))
    (pair e (pair left-unit-e right-unit-e))
    (pair e' (pair left-unit-e' right-unit-e')) =
    eq-subtype
      ( λ e → is-prop-prod
        ( is-prop-Π (λ y → is-set-X (μ e y) y))
        ( is-prop-Π (λ x → is-set-X (μ x e) x)))
      ( (inv (left-unit-e' e)) ∙ (right-unit-e e'))

abstract
  is-prop-is-unital :
    {l : Level} (G : Semi-Group l) → is-prop (is-unital G)
  is-prop-is-unital G = is-prop-is-prop' (is-prop-is-unital' G)

{- The property that a monoid is a group is just the property that the monoid
   that every element is invertible, i.e., it comes equipped with an inverse
   operation that satisfies the left and right inverse laws. -}

is-group' :
  {l : Level} (G : Semi-Group l) → is-unital G → UU l
is-group' G is-unital-G =
  Σ ( type-Semi-Group G → type-Semi-Group G)
    ( λ i →
      ( (x : type-Semi-Group G) →
        Id (mul-Semi-Group G (i x) x) (pr1 is-unital-G)) ×
      ( (x : type-Semi-Group G) →
        Id (mul-Semi-Group G x (i x)) (pr1 is-unital-G)))

is-group :
  {l : Level} (G : Semi-Group l) → UU l
is-group G =
  Σ (is-unital G) (is-group' G)

Group :
  (l : Level) → UU (lsuc l)
Group l = Σ (Semi-Group l) is-group

{- Some bureaucracy of Groups. -}

semi-group-Group :
  {l : Level} → Group l → Semi-Group l
semi-group-Group G = pr1 G

set-Group :
  {l : Level} → Group l → UU-Set l
set-Group G = pr1 (semi-group-Group G)

type-Group :
  {l : Level} → Group l → UU l
type-Group G = pr1 (set-Group G)

is-set-type-Group :
  {l : Level} (G : Group l) → is-set (type-Group G)
is-set-type-Group G = pr2 (set-Group G)

associative-mul-Group :
  {l : Level} (G : Group l) → has-associative-mul (set-Group G)
associative-mul-Group G = pr2 (semi-group-Group G)

mul-Group :
  {l : Level} (G : Group l) →
  type-Group G → type-Group G → type-Group G
mul-Group G = pr1 (associative-mul-Group G)

is-associative-mul-Group :
  {l : Level} (G : Group l) (x y z : type-Group G) →
  Id (mul-Group G (mul-Group G x y) z) (mul-Group G x (mul-Group G y z))
is-associative-mul-Group G = pr2 (associative-mul-Group G)

is-group-Group :
  {l : Level} (G : Group l) → is-group (semi-group-Group G)
is-group-Group G = pr2 G

is-unital-Group :
  {l : Level} (G : Group l) → is-unital (semi-group-Group G)
is-unital-Group G = pr1 (is-group-Group G)

unit-Group :
  {l : Level} (G : Group l) → type-Group G
unit-Group G = pr1 (is-unital-Group G)

left-unit-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G (unit-Group G) x) x
left-unit-law-Group G = pr1 (pr2 (is-unital-Group G))

right-unit-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G x (unit-Group G)) x
right-unit-law-Group G = pr2 (pr2 (is-unital-Group G))

has-inverses-Group :
  {l : Level} (G : Group l) →
  is-group' (semi-group-Group G) (is-unital-Group G)
has-inverses-Group G = pr2 (is-group-Group G)

inv-Group :
  {l : Level} (G : Group l) →
  type-Group G → type-Group G
inv-Group G = pr1 (has-inverses-Group G)

left-inverse-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G (inv-Group G x) x) (unit-Group G)
left-inverse-law-Group G = pr1 (pr2 (has-inverses-Group G))

right-inverse-law-Group :
  {l : Level} (G : Group l) (x : type-Group G) →
  Id (mul-Group G x (inv-Group G x)) (unit-Group G)
right-inverse-law-Group G = pr2 (pr2 (has-inverses-Group G))

{- We show that being a group is a proposition. -}

abstract
  is-prop-is-group' :
    {l : Level} (G : Semi-Group l) (e : is-unital G) → is-prop' (is-group' G e)
  is-prop-is-group'
    ( pair (pair G is-set-G) (pair μ assoc-G))
    ( pair e (pair left-unit-G right-unit-G))
    ( pair i (pair left-inv-i right-inv-i))
    ( pair i' (pair left-inv-i' right-inv-i')) =
    eq-subtype
      ( λ i →
        is-prop-prod
          ( is-prop-Π (λ x → is-set-G (μ (i x) x) e))
          ( is-prop-Π (λ x → is-set-G (μ x (i x)) e)))
      ( eq-htpy
        ( λ x →                                             -- ix
          ( inv (left-unit-G (i x))) ∙                      -- = 1·(ix)
          ( ( ap (λ y → μ y (i x)) (inv (left-inv-i' x))) ∙ -- = (i'x·x)·(ix)
            ( ( assoc-G (i' x) x (i x)) ∙                   -- = (i'x)·(x·i'x)
              ( ( ap (μ (i' x)) (right-inv-i x)) ∙          -- = (i'x)·1
                ( right-unit-G (i' x)))))))                 -- = i'x

abstract
  is-prop-is-group :
    {l : Level} (G : Semi-Group l) → is-prop (is-group G)
  is-prop-is-group G =
    is-prop-Σ
      ( is-prop-is-unital G)
      ( λ e → is-prop-is-prop' (is-prop-is-group' G e))

{- We give two examples of groups. The first is the group ℤ of integers. The
   second is the loop space of a pointed 1-type.  -}

{- The group of integers. -}

semi-group-ℤ : Semi-Group lzero
semi-group-ℤ = pair set-ℤ (pair add-ℤ associative-add-ℤ)

group-ℤ : Group lzero
group-ℤ =
  pair
    ( semi-group-ℤ)
    ( pair
      ( pair zero-ℤ (pair left-unit-law-add-ℤ right-unit-law-add-ℤ))
      ( pair neg-ℤ (pair left-inverse-law-add-ℤ right-inverse-law-add-ℤ)))

{- The loop space of a 1-type as a group. -}

loop-space :
  {l : Level} {A : UU l} → A → UU l
loop-space a = Id a a

set-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → UU-Set l
set-loop-space A a is-set-Ω = pair (Id a a) is-set-Ω

semi-group-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → Semi-Group l
semi-group-loop-space A a is-set-Ω =
  pair
    ( set-loop-space A a is-set-Ω)
    ( pair (λ p q → p ∙ q) assoc)

group-loop-space :
  {l : Level} (A : UU l) (a : A) (is-set-Ω : is-set (Id a a)) → Group l
group-loop-space A a is-set-Ω =
  pair
    ( semi-group-loop-space A a is-set-Ω)
    ( pair
      ( pair refl (pair (λ q → left-unit) (λ p → right-unit)))
      ( pair inv (pair left-inv right-inv)))

set-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → UU-Set l
set-loop-space-1-type (pair A is-1-type-A) a =
  set-loop-space A a (is-1-type-A a a)

semi-group-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → Semi-Group l
semi-group-loop-space-1-type (pair A is-1-type-A) a =
  semi-group-loop-space A a (is-1-type-A a a)

group-loop-space-1-type :
  {l : Level} (A : 1-type l) (a : pr1 A) → Group l
group-loop-space-1-type (pair A is-1-type-A) a =
  group-loop-space A a (is-1-type-A a a)

{- We introduce the automorphism group on a set X. -}

aut-Set :
  {l : Level} (X : UU-Set l) → UU-Set l
aut-Set X = set-equiv X X

associative-comp-equiv :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} →
  (e : A ≃ B) (f : B ≃ C) (g : C ≃ D) →
  Id ((g ∘e f) ∘e e) (g ∘e (f ∘e e))
associative-comp-equiv e f g = eq-htpy-equiv refl-htpy

has-associative-mul-aut-Set :
  {l : Level} (X : UU-Set l) → has-associative-mul (aut-Set X)
has-associative-mul-aut-Set X =
  pair
    ( λ e f → f ∘e e)
    ( λ e f g → inv (associative-comp-equiv e f g))

aut-Semi-Group :
  {l : Level} (X : UU-Set l) → Semi-Group l
aut-Semi-Group X =
  pair
    ( aut-Set X)
    ( has-associative-mul-aut-Set X)

left-unit-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id ((equiv-id Y) ∘e e) e
left-unit-law-equiv e = eq-htpy-equiv refl-htpy

right-unit-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id (e ∘e (equiv-id X)) e
right-unit-law-equiv e = eq-htpy-equiv refl-htpy

is-unital-aut-Semi-Group :
  {l : Level} (X : UU-Set l) → is-unital (aut-Semi-Group X)
is-unital-aut-Semi-Group X =
  pair
    ( equiv-id (type-Set X))
    ( pair
      ( right-unit-law-equiv)
      ( left-unit-law-equiv))

left-inverse-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id ((inv-equiv e) ∘e e) (equiv-id X)
left-inverse-law-equiv e =
  eq-htpy-equiv (isretr-inv-is-equiv (is-equiv-map-equiv e))

right-inverse-law-equiv :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) →
  Id (e ∘e (inv-equiv e)) (equiv-id Y)
right-inverse-law-equiv e =
  eq-htpy-equiv (issec-inv-is-equiv (is-equiv-map-equiv e))

is-group-aut-Semi-Group' :
  {l : Level} (X : UU-Set l) →
  is-group' (aut-Semi-Group X) (is-unital-aut-Semi-Group X)
is-group-aut-Semi-Group' X =
  pair
    ( inv-equiv)
    ( pair right-inverse-law-equiv left-inverse-law-equiv)

aut-Group :
  {l : Level} → UU-Set l → Group l
aut-Group X =
  pair
    ( aut-Semi-Group X)
    ( pair (is-unital-aut-Semi-Group X) (is-group-aut-Semi-Group' X))

{- Now we introduce homomorphisms of semi-groups. Group homomorphisms are just
   homomorphisms between their underlying semi-groups. -}

preserves-mul :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  (type-Semi-Group G → type-Semi-Group H) → UU (l1 ⊔ l2)
preserves-mul G H f =
  (x y : type-Semi-Group G) →
      Id (f (mul-Semi-Group G x y)) (mul-Semi-Group H (f x) (f y))

abstract
  is-prop-preserves-mul :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : type-Semi-Group G → type-Semi-Group H) →
    is-prop (preserves-mul G H f)
  is-prop-preserves-mul G (pair (pair H is-set-H) (pair μ-H assoc-H)) f =
    is-prop-Π (λ x →
      is-prop-Π (λ y →
        is-set-H (f (mul-Semi-Group G x y)) (μ-H (f x) (f y))))

hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
hom-Semi-Group G H =
  Σ ( type-Semi-Group G → type-Semi-Group H)
    ( preserves-mul G H)

{- Bureaucracy of homomorphisms of semi-groups. -}

map-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( hom-Semi-Group G H) →
  ( type-Semi-Group G) → (type-Semi-Group H)
map-hom-Semi-Group G H f = pr1 f

preserves-mul-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) →
  preserves-mul G H (map-hom-Semi-Group G H f)
preserves-mul-hom-Semi-Group G H f = pr2 f

{- We characterize the identity type of the semi-group homomorphisms. -}

htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  (f g : hom-Semi-Group G H) → UU (l1 ⊔ l2)
htpy-hom-Semi-Group G H f g =
  (map-hom-Semi-Group G H f) ~ (map-hom-Semi-Group G H g)

reflexive-htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) → htpy-hom-Semi-Group G H f f
reflexive-htpy-hom-Semi-Group G H f = refl-htpy

htpy-hom-Semi-Group-eq :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f g : hom-Semi-Group G H) → Id f g → htpy-hom-Semi-Group G H f g
htpy-hom-Semi-Group-eq G H f .f refl = reflexive-htpy-hom-Semi-Group G H f

abstract
  is-contr-total-htpy-hom-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) →
    is-contr (Σ (hom-Semi-Group G H) (htpy-hom-Semi-Group G H f))
  is-contr-total-htpy-hom-Semi-Group G H f =
    is-contr-total-Eq-substructure
      ( is-contr-total-htpy (map-hom-Semi-Group G H f))
      ( is-prop-preserves-mul G H)
      ( map-hom-Semi-Group G H f)
      ( refl-htpy)
      ( preserves-mul-hom-Semi-Group G H f)

abstract
  is-equiv-htpy-hom-Semi-Group-eq :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f g : hom-Semi-Group G H) → is-equiv (htpy-hom-Semi-Group-eq G H f g)
  is-equiv-htpy-hom-Semi-Group-eq G H f =
    fundamental-theorem-id f
      ( reflexive-htpy-hom-Semi-Group G H f)
      ( is-contr-total-htpy-hom-Semi-Group G H f)
      ( htpy-hom-Semi-Group-eq G H f)

eq-htpy-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  { f g : hom-Semi-Group G H} → htpy-hom-Semi-Group G H f g → Id f g
eq-htpy-hom-Semi-Group G H {f} {g} =
  inv-is-equiv (is-equiv-htpy-hom-Semi-Group-eq G H f g)

{- We show that the type of semi-group homomorphisms between two semi-groups is
   a set. -}

is-set-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  is-set (hom-Semi-Group G H)
is-set-hom-Semi-Group G H (pair f μ-f) (pair g μ-g) =
  is-prop-is-equiv
    ( htpy-hom-Semi-Group G H (pair f μ-f) (pair g μ-g))
    ( htpy-hom-Semi-Group-eq G H (pair f μ-f) (pair g μ-g))
    ( is-equiv-htpy-hom-Semi-Group-eq G H (pair f μ-f) (pair g μ-g))
    ( is-prop-Π (λ x → is-set-type-Semi-Group H (f x) (g x)))

{- We introduce group homomorphisms. -}

hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
hom-Group G H =
  hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

{- Bureaucracy of group homomorphisms. -}

map-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( hom-Group G H) →
  ( type-Group G) → (type-Group H)
map-hom-Group G H f = pr1 f

preserves-mul-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) →
  preserves-mul
    ( semi-group-Group G)
    ( semi-group-Group H)
    ( map-hom-Group G H f)
preserves-mul-hom-Group G H f = pr2 f

{- We characterize the identity type of the group homomorphisms. -}

htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2)
  (f g : hom-Group G H) → UU (l1 ⊔ l2)
htpy-hom-Group G H =
  htpy-hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

reflexive-htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) → htpy-hom-Group G H f f
reflexive-htpy-hom-Group G H =
  reflexive-htpy-hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

htpy-hom-Group-eq :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f g : hom-Group G H) → Id f g → htpy-hom-Group G H f g
htpy-hom-Group-eq G H =
  htpy-hom-Semi-Group-eq
    ( semi-group-Group G)
    ( semi-group-Group H)

abstract
  is-contr-total-htpy-hom-Group :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) →
    is-contr (Σ (hom-Group G H) (htpy-hom-Group G H f))
  is-contr-total-htpy-hom-Group G H =
    is-contr-total-htpy-hom-Semi-Group
      ( semi-group-Group G)
      ( semi-group-Group H)

abstract
  is-equiv-htpy-hom-Group-eq :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f g : hom-Group G H) → is-equiv (htpy-hom-Group-eq G H f g)
  is-equiv-htpy-hom-Group-eq G H =
    is-equiv-htpy-hom-Semi-Group-eq
      ( semi-group-Group G)
      ( semi-group-Group H)

eq-htpy-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  { f g : hom-Group G H} → htpy-hom-Group G H f g → Id f g
eq-htpy-hom-Group G H =
  eq-htpy-hom-Semi-Group (semi-group-Group G) (semi-group-Group H)

{- Next, we construct the identity group homomorphism, and we show that
   compositions of group homomorphisms are again group homomorphisms. -}

preserves-mul-id :
  {l : Level} (G : Semi-Group l) → preserves-mul G G id
preserves-mul-id (pair (pair G is-set-G) (pair μ-G assoc-G)) x y = refl

id-Semi-Group :
  {l : Level} (G : Semi-Group l) → hom-Semi-Group G G
id-Semi-Group G =
  pair id (preserves-mul-id G)

id-Group :
  {l : Level} (G : Group l) → hom-Group G G
id-Group G = id-Semi-Group (semi-group-Group G)

composition-Semi-Group :
  {l1 l2 l3 : Level} →
  (G : Semi-Group l1) (H : Semi-Group l2) (K : Semi-Group l3) →
  (hom-Semi-Group H K) → (hom-Semi-Group G H) → (hom-Semi-Group G K)
composition-Semi-Group G H K (pair g μ-g) (pair f μ-f) =
  pair
    ( g ∘ f)
    ( λ x y → (ap g (μ-f x y)) ∙ (μ-g (f x) (f y)))

composition-Group :
  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (K : Group l3) →
  (hom-Group H K) → (hom-Group G H) → (hom-Group G K)
composition-Group G H K =
  composition-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)
    ( semi-group-Group K)

{- Next, we prove the that the laws for a category hold for group homomorphisms,
   i.e., we show that composition is associative and satisfies the left and
   right unit laws. Before we show that these laws hold, we will characterize
   the identity type of the types of semi-group homomorphisms and group
   homomorphisms. -}

associative-Semi-Group :
  { l1 l2 l3 l4 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( K : Semi-Group l3) (L : Semi-Group l4) (h : hom-Semi-Group K L) →
  ( g : hom-Semi-Group H K) (f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G H L
       ( composition-Semi-Group H K L h g) f)
     ( composition-Semi-Group G K L h
       ( composition-Semi-Group G H K g f))
associative-Semi-Group G H K L (pair h μ-h) (pair g μ-g) (pair f μ-f) =
  eq-htpy-hom-Semi-Group G L refl-htpy

left-unit-law-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G H H (id-Semi-Group H) f) f
left-unit-law-Semi-Group G
  (pair (pair H is-set-H) (pair μ-H assoc-H)) (pair f μ-f) =
  eq-htpy-hom-Semi-Group G
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( refl-htpy)

right-unit-law-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2)
  ( f : hom-Semi-Group G H) →
  Id ( composition-Semi-Group G G H f (id-Semi-Group G)) f
right-unit-law-Semi-Group
  (pair (pair G is-set-G) (pair μ-G assoc-G)) H (pair f μ-f) =
  eq-htpy-hom-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G)) H refl-htpy

{- Now we introduce the notion of group isomorphism. Finally, we will show that
   isomorphic groups are equal. -}

is-iso-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
  ( f : hom-Semi-Group G H) → UU (l1 ⊔ l2)
is-iso-Semi-Group G H f =
  Σ ( hom-Semi-Group H G) (λ g →
    ( Id (composition-Semi-Group H G H f g) (id-Semi-Group H)) ×
    ( Id (composition-Semi-Group G H G g f) (id-Semi-Group G)))

iso-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
iso-Semi-Group G H =
  Σ (hom-Semi-Group G H) (is-iso-Semi-Group G H)

abstract
  is-prop-is-iso-Semi-Group' :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) → is-prop' (is-iso-Semi-Group G H f)
  is-prop-is-iso-Semi-Group' G H f
    (pair g (pair issec isretr)) (pair g' (pair issec' isretr')) =
    eq-subtype
      ( λ h →
        is-prop-prod
          ( is-set-hom-Semi-Group H H
            ( composition-Semi-Group H G H f h)
            ( id-Semi-Group H))
          ( is-set-hom-Semi-Group G G
            ( composition-Semi-Group G H G h f)
            ( id-Semi-Group G)))
      ( ( inv (left-unit-law-Semi-Group H G g)) ∙
        ( ( inv (ap (λ h → composition-Semi-Group H G G h g) isretr')) ∙
          ( ( associative-Semi-Group H G H G g' f g) ∙
            ( ( ap (composition-Semi-Group H H G g') issec) ∙
              ( right-unit-law-Semi-Group H G g')))))

abstract
  is-prop-is-iso-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) → is-prop (is-iso-Semi-Group G H f)
  is-prop-is-iso-Semi-Group G H f =
    is-prop-is-prop' (is-prop-is-iso-Semi-Group' G H f)

abstract
  preserves-mul-inv-is-equiv-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H)
    ( is-equiv-f : is-equiv (map-hom-Semi-Group G H f)) →
    preserves-mul H G (inv-is-equiv is-equiv-f)
  preserves-mul-inv-is-equiv-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f) is-equiv-f x y =
    inv-is-equiv
      ( is-emb-is-equiv f is-equiv-f
        ( inv-is-equiv is-equiv-f (μ-H x y))
        ( μ-G (inv-is-equiv is-equiv-f x) (inv-is-equiv is-equiv-f y)))
      ( ( ( issec-inv-is-equiv is-equiv-f (μ-H x y)) ∙
          ( ( ap (λ t → μ-H t y) (inv (issec-inv-is-equiv is-equiv-f x))) ∙
            ( ap
              ( μ-H (f (inv-is-equiv is-equiv-f x)))
              ( inv (issec-inv-is-equiv is-equiv-f y))))) ∙
        ( inv (μ-f (inv-is-equiv is-equiv-f x) (inv-is-equiv is-equiv-f y))))

abstract
  is-iso-is-equiv-hom-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) (is-equiv-f : is-equiv (pr1 f)) →
    is-iso-Semi-Group G H f
  is-iso-is-equiv-hom-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f) is-equiv-f =
    pair
      ( pair
        ( inv-is-equiv is-equiv-f)
        ( preserves-mul-inv-is-equiv-Semi-Group
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( pair f μ-f) is-equiv-f))
      ( pair
        ( eq-htpy-hom-Semi-Group
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( pair (pair H is-set-H) (pair μ-H assoc-H))
          ( issec-inv-is-equiv is-equiv-f))
        ( eq-htpy-hom-Semi-Group
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( pair (pair G is-set-G) (pair μ-G assoc-G))
          ( isretr-inv-is-equiv is-equiv-f)))

abstract
  is-equiv-hom-is-iso-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    ( f : hom-Semi-Group G H) (is-iso-f : is-iso-Semi-Group G H f) →
    ( is-equiv (pr1 f))
  is-equiv-hom-is-iso-Semi-Group
    ( pair (pair G is-set-G) (pair μ-G assoc-G))
    ( pair (pair H is-set-H) (pair μ-H assoc-H))
    ( pair f μ-f)
    ( pair (pair g μ-g) (pair issec isretr)) =
    is-equiv-has-inverse g
      ( htpy-eq (ap pr1 issec))
      ( htpy-eq (ap pr1 isretr))

equiv-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
equiv-Semi-Group G H =
  Σ ( type-Semi-Group G ≃ type-Semi-Group H)
    ( λ e → preserves-mul G H (map-equiv e))

total-is-equiv-hom-Semi-Group :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
total-is-equiv-hom-Semi-Group G H =
  Σ (hom-Semi-Group G H) (λ f → is-equiv (map-hom-Semi-Group G H f))

preserves-mul' :
  { l1 l2 : Level} (G : Semi-Group l1) (H : UU-Set l2)
  ( μ-H : has-associative-mul H) →
  ( e : (type-Semi-Group G) ≃ (type-Set H)) →
  UU (l1 ⊔ l2)
preserves-mul' G H μ-H e = preserves-mul G (pair H μ-H) (map-equiv e)

equiv-Semi-Group' :
  { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) → UU (l1 ⊔ l2)
equiv-Semi-Group' G H = equiv-Semi-Group G (pair (pr1 H) (pr2 H))

abstract
  equiv-iso-Semi-Group-equiv-Semi-Group :
    { l1 l2 : Level} (G : Semi-Group l1) (H : Semi-Group l2) →
    equiv-Semi-Group' G H ≃ iso-Semi-Group G H
  equiv-iso-Semi-Group-equiv-Semi-Group G H =
    ( ( ( equiv-total-subtype
          ( λ f → is-subtype-is-equiv (map-hom-Semi-Group G H f))
          ( is-prop-is-iso-Semi-Group G H)
          ( is-iso-is-equiv-hom-Semi-Group G H)
          ( is-equiv-hom-is-iso-Semi-Group G H)) ∘e
        ( ( inv-equiv
            ( equiv-Σ-assoc
              ( type-Semi-Group G → type-Semi-Group H)
              ( preserves-mul G H)
              ( λ f → is-equiv (map-hom-Semi-Group G H f)))) ∘e
          ( equiv-tot
            ( λ f → equiv-swap-prod (is-equiv f) (preserves-mul G H f))))) ∘e
      ( equiv-Σ-assoc
        ( type-Semi-Group G → type-Semi-Group H)
        ( is-equiv)
        ( λ e → preserves-mul G H (map-equiv e)))) ∘e
    ( equiv-tr (equiv-Semi-Group G) (η-pair H))

center-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  Σ (has-associative-mul (pr1 G)) (λ μ → preserves-mul G (pair (pr1 G) μ) id)
center-total-preserves-mul-id (pair (pair G is-set-G) (pair μ-G assoc-G)) =
  pair (pair μ-G assoc-G) (λ x y → refl)

contraction-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  ( t : Σ ( has-associative-mul (pr1 G))
          ( λ μ → preserves-mul G (pair (pr1 G) μ) id)) →
  Id (center-total-preserves-mul-id G) t
contraction-total-preserves-mul-id
  ( pair (pair G is-set-G) (pair μ-G assoc-G))
  ( pair (pair μ-G' assoc-G') μ-id) =
  eq-subtype
    ( λ μ →
      is-prop-preserves-mul
        ( pair (pair G is-set-G) (pair μ-G assoc-G))
        ( pair (pair G is-set-G) μ) id)
    ( eq-subtype
      ( λ μ →
        is-prop-Π (λ x →
          is-prop-Π (λ y →
            is-prop-Π (λ z →
              is-set-G (μ (μ x y) z) (μ x (μ y z))))))
      ( eq-htpy (λ x → eq-htpy (λ y → μ-id x y))))

is-contr-total-preserves-mul-id :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (has-associative-mul (pr1 G)) (λ μ → preserves-mul G (pair (pr1 G) μ) id))
is-contr-total-preserves-mul-id G =
  pair
    ( center-total-preserves-mul-id G)
    ( contraction-total-preserves-mul-id G)

is-contr-total-equiv-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (Semi-Group l1) (λ H → equiv-Semi-Group' G H))
is-contr-total-equiv-Semi-Group {l1} G =
  is-contr-total-Eq-structure
    ( preserves-mul' G)
    ( is-contr-total-Eq-substructure
      ( is-contr-total-equiv (type-Semi-Group G))
      ( is-prop-is-set)
      ( type-Semi-Group G)
      ( equiv-id (type-Semi-Group G))
      ( is-set-type-Semi-Group G))
    ( pair (pr1 G) (equiv-id (type-Semi-Group G)))
    ( is-contr-total-preserves-mul-id G)

is-contr-total-iso-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) →
  is-contr (Σ (Semi-Group l1) (iso-Semi-Group G))
is-contr-total-iso-Semi-Group {l1} G =
  is-contr-equiv'
    ( Σ (Semi-Group l1) (λ H → equiv-Semi-Group' G H))
    ( equiv-tot (λ H → equiv-iso-Semi-Group-equiv-Semi-Group G H))
    ( is-contr-total-equiv-Semi-Group G)

iso-id-Semi-Group :
  { l1 : Level} (G : Semi-Group l1) → iso-Semi-Group G G
iso-id-Semi-Group G =
  pair
    ( id-Semi-Group G)
    ( pair
      ( id-Semi-Group G)
      ( pair
        ( left-unit-law-Semi-Group G G (id-Semi-Group G))
        ( right-unit-law-Semi-Group G G (id-Semi-Group G))))

iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → Id G H → iso-Semi-Group G H
iso-eq-Semi-Group G .G refl = iso-id-Semi-Group G

is-equiv-iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → is-equiv (iso-eq-Semi-Group G H)
is-equiv-iso-eq-Semi-Group G =
  fundamental-theorem-id G
    ( iso-id-Semi-Group G)
    ( is-contr-total-iso-Semi-Group G)
    ( iso-eq-Semi-Group G)

equiv-iso-eq-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → Id G H ≃ iso-Semi-Group G H
equiv-iso-eq-Semi-Group G H =
  pair (iso-eq-Semi-Group G H) (is-equiv-iso-eq-Semi-Group G H)

eq-iso-Semi-Group :
  { l1 : Level} (G H : Semi-Group l1) → iso-Semi-Group G H → Id G H
eq-iso-Semi-Group G H = inv-is-equiv (is-equiv-iso-eq-Semi-Group G H)

{- Finally we show that isomorphic groups are equal. -}

iso-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
iso-Group G H =
  iso-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)

iso-id-Group :
  { l1 : Level} (G : Group l1) → iso-Group G G
iso-id-Group G = iso-id-Semi-Group (semi-group-Group G)

iso-eq-Group :
  { l1 : Level} (G H : Group l1) → Id G H → iso-Group G H
iso-eq-Group G .G refl = iso-id-Group G

abstract
  equiv-iso-eq-Group' :
    { l1 : Level} (G H : Group l1) → Id G H ≃ iso-Group G H
  equiv-iso-eq-Group' G H =
    ( equiv-iso-eq-Semi-Group
      ( semi-group-Group G)
      ( semi-group-Group H)) ∘e
    ( equiv-ap-pr1-is-subtype is-prop-is-group {s = G} {t = H})

abstract
  is-contr-total-iso-Group :
    { l1 : Level} (G : Group l1) → is-contr (Σ (Group l1) (iso-Group G))
  is-contr-total-iso-Group {l1} G =
    is-contr-equiv'
      ( Σ (Group l1) (Id G))
      ( equiv-tot (λ H → equiv-iso-eq-Group' G H))
      ( is-contr-total-path G)

is-equiv-iso-eq-Group :
  { l1 : Level} (G H : Group l1) → is-equiv (iso-eq-Group G H)
is-equiv-iso-eq-Group G =
  fundamental-theorem-id G
    ( iso-id-Group G)
    ( is-contr-total-iso-Group G)
    ( iso-eq-Group G)

eq-iso-Group :
  { l1 : Level} (G H : Group l1) → iso-Group G H → Id G H
eq-iso-Group G H = inv-is-equiv (is-equiv-iso-eq-Group G H)

-- Categories

underlying-type-Set :
  {l : Level} → UU-Set l → UU l
underlying-type-Set A = pr1 A

is-set-underlying-type-Set :
  {l : Level} (A : UU-Set l) → is-set (underlying-type-Set A)
is-set-underlying-type-Set A = pr2 A

associative-composition-structure :
  {l1 l2 : Level} (A : UU l1) (hom : A → A → UU-Set l2) → UU (l1 ⊔ l2)
associative-composition-structure A hom =
  Σ ( (x y z : A)
      → underlying-type-Set (hom x y)
      → underlying-type-Set (hom y z)
      → underlying-type-Set (hom x z))
    ( λ μ → (x y z w : A) (f : underlying-type-Set (hom x y)) (g : underlying-type-Set (hom y z)) (h : underlying-type-Set (hom z w)) →
      Id (μ x z w (μ x y z f g) h) (μ x y w f (μ y z w g h)))

is-unital-composition-structure :
  {l1 l2 : Level} (A : UU l1) (hom : A → A → UU-Set l2) →
  associative-composition-structure A hom → UU _
is-unital-composition-structure A hom (pair μ assoc-μ) =
  Σ ( (x : A) → underlying-type-Set (hom x x))
    ( λ e →
      ( (x y : A) (f : underlying-type-Set (hom x y)) → Id (μ x x y (e x) f) f)
      × ( (x y : A) (f : underlying-type-Set (hom x y)) → Id (μ x y y f (e y)) f))

is-prop-is-unital-composition-structure' :
  {l1 l2 : Level} (A : UU l1) (hom : A → A → UU-Set l2) →
  ( μ : associative-composition-structure A hom) →
  is-prop' (is-unital-composition-structure A hom μ)
is-prop-is-unital-composition-structure' A hom
  ( pair μ assoc-μ)
  ( pair e (pair left-unit-law-e right-unit-law-e))
  ( pair e' (pair left-unit-law-e' right-unit-law-e')) =
  eq-subtype
    ( λ x →
      is-prop-prod
        ( is-prop-Π
          ( λ a → is-prop-Π
            ( λ b → is-prop-Π
              ( λ f' →
                is-set-underlying-type-Set (hom a b) (μ a a b (x a) f') f'))))
        ( is-prop-Π
          ( λ a → is-prop-Π
            ( λ b → is-prop-Π
              ( λ f' →
                is-set-underlying-type-Set (hom a b) (μ a b b f' (x b)) f')))))
    ( eq-htpy
      ( λ x → (inv (left-unit-law-e' x x (e x))) ∙ right-unit-law-e x x (e' x)))

Precategory :
  (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Precategory l1 l2 =
  Σ ( UU l1) (λ A →
    Σ (A → A → UU-Set l2) (λ hom →
      Σ ( associative-composition-structure A hom)
        ( is-unital-composition-structure A hom)))

obj-Precat :
  {l1 l2 : Level} → Precategory l1 l2 → UU l1
obj-Precat C = pr1 C

hom-Set-Precat :
  {l1 l2 : Level} (C : Precategory l1 l2) (x y : obj-Precat C) → UU-Set l2
hom-Set-Precat C = pr1 (pr2 C)

hom-Precat :
  {l1 l2 : Level} (C : Precategory l1 l2) (x y : obj-Precat C) → UU l2
hom-Precat C x y = pr1 (hom-Set-Precat C x y)

is-set-hom-Precat :
  {l1 l2 : Level} (C : Precategory l1 l2) (x y : obj-Precat C) →
  is-set (hom-Precat C x y)
is-set-hom-Precat C x y = pr2 (hom-Set-Precat C x y)

associative-composition-Precat :
  {l1 l2 : Level} (C : Precategory l1 l2) →
  associative-composition-structure (obj-Precat C) (hom-Set-Precat C)
associative-composition-Precat C = pr1 (pr2 (pr2 C))

composition-Precat :
  {l1 l2 : Level} (C : Precategory l1 l2) {x y z : obj-Precat C} →
  hom-Precat C x y → hom-Precat C y z → hom-Precat C x z
composition-Precat C {x} {y} {z} =
  pr1 (associative-composition-Precat C) x y z

is-associative-composition-Precat :
  { l1 l2 : Level} (C : Precategory l1 l2) {x y z w : obj-Precat C} →
  ( f : hom-Precat C x y) (g : hom-Precat C y z) (h : hom-Precat C z w) →
  Id (composition-Precat C (composition-Precat C f g) h)
     (composition-Precat C f (composition-Precat C g h))
is-associative-composition-Precat C {x} {y} {z} {w} =
  pr2 (associative-composition-Precat C) x y z w

is-unital-Precat :
  { l1 l2 : Level} (C : Precategory l1 l2) →
  is-unital-composition-structure
    ( obj-Precat C)
    ( hom-Set-Precat C)
    ( associative-composition-Precat C)
is-unital-Precat C = pr2 (pr2 (pr2 C))

id-Precat :
  { l1 l2 : Level} (C : Precategory l1 l2) {x : obj-Precat C} →
  hom-Precat C x x
id-Precat (pair A (pair hom (pair (pair μ assoc-μ) t))) {x} =
  pr1 (is-unital-Precat {!!}) x

-- Exercises

-- Exercise

{- We show that group homomorphisms preserve the unit. -}

preserves-unit :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Semi-Group
    ( semi-group-Group G)
    ( semi-group-Group H)) →
  UU l2
preserves-unit G H f =
  Id (map-hom-Group G H f (unit-Group G)) (unit-Group H)

abstract
  preserves-unit-group-hom :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) → preserves-unit G H f
  preserves-unit-group-hom
    ( pair ( pair (pair G is-set-G) (pair μ-G assoc-G))
           ( pair ( pair e-G (pair left-unit-G right-unit-G))
                  ( pair i-G (pair left-inv-G right-inv-G))))
    ( pair ( pair (pair H is-set-H) (pair μ-H assoc-H))
           ( pair ( pair e-H (pair left-unit-H right-unit-H))
                  ( pair i-H (pair left-inv-H right-inv-H))))
    ( pair f μ-f) =
    ( inv (left-unit-H (f e-G))) ∙
    ( ( ap (λ x → μ-H x (f e-G)) (inv (left-inv-H (f e-G)))) ∙
      ( ( assoc-H (i-H (f e-G)) (f e-G) (f e-G)) ∙
        ( ( ap (μ-H (i-H (f e-G))) (inv (μ-f e-G e-G))) ∙
          ( ( ap (λ x → μ-H (i-H (f e-G)) (f x)) (left-unit-G e-G)) ∙
            ( left-inv-H (f e-G))))))

{- We show that group homomorphisms preserve inverses. -}

preserves-inverses :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  ( f : hom-Group G H) → UU (l1 ⊔ l2)
preserves-inverses G H f =
  ( x : type-Group G) →
  Id ( map-hom-Group G H f (inv-Group G x))
     ( inv-Group H (map-hom-Group G H f x))

abstract
  preserves-inverses-group-hom' :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) →
    preserves-unit G H f → preserves-inverses G H f
  preserves-inverses-group-hom'
    ( pair ( pair (pair G is-set-G) (pair μ-G assoc-G))
           ( pair ( pair e-G (pair left-unit-G right-unit-G))
                  ( pair i-G (pair left-inv-G right-inv-G))))
    ( pair ( pair (pair H is-set-H) (pair μ-H assoc-H))
           ( pair ( pair e-H (pair left-unit-H right-unit-H))
                  ( pair i-H (pair left-inv-H right-inv-H))))
    ( pair f μ-f) preserves-unit-f x =
    ( inv ( right-unit-H (f (i-G x)))) ∙
    ( ( ap (μ-H (f (i-G x))) (inv (right-inv-H (f x)))) ∙
      ( ( inv (assoc-H (f (i-G x)) (f x) (i-H (f x)))) ∙
        ( ( inv (ap (λ y → μ-H y (i-H (f x))) (μ-f (i-G x) x))) ∙
          ( ( ap (λ y → μ-H (f y) (i-H (f x))) (left-inv-G x)) ∙
            ( ( ap
                ( λ y → μ-H y (i-H (f x)))
                ( preserves-unit-f)) ∙
              ( left-unit-H (i-H (f x))))))))

abstract
  preserves-inverses-group-hom :
    { l1 l2 : Level} (G : Group l1) (H : Group l2) →
    ( f : hom-Group G H) → preserves-inverses G H f
  preserves-inverses-group-hom G H f =
    preserves-inverses-group-hom' G H f (preserves-unit-group-hom G H f)

hom-Group' :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) → UU (l1 ⊔ l2)
hom-Group' G H =
  Σ ( hom-Group G H) (λ f →
    ( preserves-unit G H f) × (preserves-inverses G H f))

preserves-all-hom-Group :
  { l1 l2 : Level} (G : Group l1) (H : Group l2) →
  hom-Group G H → hom-Group' G H
preserves-all-hom-Group G H f =
  pair f
    ( pair
      ( preserves-unit-group-hom G H f)
      ( preserves-inverses-group-hom G H f))

-- Exercise

{-
hom-mul-Group :
  {l : Level} (G : Group l) →
  hom-Group G Aut
-}

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
-- Andreas Abel, 2022-06-06, issue #5944 reported by Mike Shulman
-- Support rewriting with 2ltt (match SSet).

{-# OPTIONS --type-in-type --rewriting --two-level #-}

open import Agda.Primitive public

postulate
  Tel   : SSet
  ε     : Tel
  _≡_   : {A : SSet} (a : A) → A → SSet
  cong  : (A B : SSet) (f : A → B) {x y : A} (p : x ≡ y) → f x ≡ f y
  coe←  : (A B : SSet) → (A ≡ B) → B → A
  el    : Tel → SSet
  []    : el ε
  ID    : (Δ : Tel) → Tel
  ID′   : (Δ : Tel) (Θ : el Δ → Tel) → Tel
  ID′ε  : (Δ : Tel) → ID′ Δ (λ _ → ε) ≡ ε

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE ID′ε #-}

postulate
  ID′-CONST   : (Θ : Tel) (Δ : Tel)

              → ID′ Θ (λ _ → Δ) ≡ ID Δ

  ID′-CONST-ε : (Θ : Tel) (δ₂ : el (ID ε))

              → coe← (el (ID′ Θ (λ _ → ε))) (el (ID ε)) (cong Tel (SSet lzero) el (ID′-CONST Θ ε)) δ₂ ≡ []

{-# REWRITE ID′-CONST-ε #-}

-- WAS: internal error when trying to make a pattern from SSet

-- Should succeed now


text:
module ASN1.Util where

open import Data.Word8 using (Word8) renaming (primWord8fromNat to to𝕎; primWord8toNat to from𝕎)
open import Data.Nat using (ℕ; _+_; _*_; _≤?_)
open import Data.Nat.DivMod using (_divMod_; result)
open import Data.Fin using (toℕ)
open import Data.List using (List; []; _∷_)
open import Relation.Nullary using (Dec; yes; no)

-- TODO: use WF induction
{-# TERMINATING #-}
base256 : ℕ → List Word8
base256 n with n ≤? 255
... | yes _ = to𝕎 n ∷ []
... | no _ with n divMod 256
... | result quotient remainder _ = to𝕎 (toℕ remainder) ∷ base256 quotient

fromBase256 : List Word8 → ℕ
fromBase256 [] = 0 -- this should not be the case, as 0 is encoded as (0 ∷ [])
fromBase256 (x ∷ ns) = from𝕎 x + 256 * fromBase256 ns

{-
base256-prop : ∀ n → n ≡ fromBase256 (base256 n)
base256-prop n with n ≤? 255
base256-prop n | yes p = {!!}
base256-prop n | no ¬p = {!!}
-}

{-# TERMINATING #-}
base128 : ℕ → List Word8
base128 n with n ≤? 127
... | yes _ = to𝕎 n ∷ []
... | no _ with n divMod 128
... | result quotient remainder _ = to𝕎 (128 + toℕ remainder) ∷ base128 quotient


text:
-- Andreas, 2014-11-08
-- This used to be a failed test case, but works now.

open import Common.Prelude

postulate
  some : Nat

data D : Nat → Set where
  d₀ : D some
  d₁ : D (suc some)

f : (n : Nat) → D n → Nat
f .some       d₀ = zero
f .(suc some) d₁ = f some d₀

-- Since  x < suc x  for all x in the structural order,
-- some < suc some  is a valid descent.


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Util.Util
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

-- This is a minimal/fake example handler that obeys the VotesOnce rule, enabling us to start
-- exploring how we express the algorithm and prove properties about it.  It simply sends a vote for
-- 1 + its LatestVotedRound, and increments its LatestVotedRound.  It is called EventProcessor for
-- historical reasons, because this what a previous version of LibraBFT called its main handler;
-- this will be updated when we move towards modeling a more recent implementation.

module LibraBFT.Impl.Consensus.ChainedBFT.EventProcessor
  (hash    : BitString → Hash)
  (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)
  where

  open RWST-do

  processCommitM : LedgerInfoWithSignatures → LBFT (List ExecutedBlock)
  processCommitM finalityProof = pure []

  fakeAuthor : Author
  fakeAuthor = 0

  fakeBlockInfo : EpochId → Round → ProposalMsg → BlockInfo
  fakeBlockInfo eid rnd pm = mkBlockInfo eid rnd (pm ^∙ pmProposal ∙ bId)

  fakeLedgerInfo : BlockInfo → ProposalMsg → LedgerInfo
  fakeLedgerInfo bi pm = mkLedgerInfo bi (pm ^∙ pmProposal ∙ bId)

  postulate
    fakeSK  : SK
    fakeSig : Signature

  processProposalMsg : Instant → ProposalMsg → LBFT Unit
  processProposalMsg inst pm = do
    st ← get
    let 𝓔  = α-EC ((₋epEC st) , (₋epEC-correct st))
        ix = EpochConfig.epochId 𝓔
        ep  = ₋epEC st
        epw = ₋epWithEC st
        epc = ₋epEC-correct st
        bt = epw ^∙ (lBlockTree 𝓔)
        nr = suc ((₋epEC st) ^∙ epLastVotedRound)
        uv = mkVote (mkVoteData (fakeBlockInfo ix nr pm) (fakeBlockInfo ix 0 pm))
                    fakeAuthor
                    (fakeLedgerInfo (fakeBlockInfo ix nr pm) pm)
                    fakeSig
                    (₋bSignature (₋pmProposal pm))
        sv =  record uv { ₋vSignature = sign ⦃ sig-Vote ⦄ uv fakeSK}
        si = mkSyncInfo (₋btHighestQuorumCert bt) (₋btHighestCommitCert bt)
        ep' = ep [ epLastVotedRound := nr ]
        epc2 = EventProcessorEC-correct-≡ (₋epEC st) ep' refl epc
        st' = record st { ₋epEC         = ep'
                        ; ₋epEC-correct = epc2
                        ; ₋epWithEC     = subst EventProcessorWithEC (α-EC-≡ ep ep' refl refl epc) epw
                        }
    put st'
    tell1 (SendVote (mkVoteMsg sv si) (fakeAuthor ∷ []))
    pure unit

  processVote : Instant → VoteMsg → LBFT Unit
  processVote now msg = pure unit

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
------------------------------------------------------------------------------
-- The Booleans properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Bool.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Bool
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Basic properties

&&-Bool : ∀ {a b} → Bool a → Bool b → Bool (a && b)
&&-Bool {b = b} btrue Bb = prf
  where postulate prf : Bool (true && b)
        {-# ATP prove prf #-}
&&-Bool {b = b} bfalse Bb = prf
  where postulate prf : Bool (false && b)
        {-# ATP prove prf #-}

not-Bool : ∀ {b} → Bool b → Bool (not b)
not-Bool btrue = prf
  where postulate prf : Bool (not true)
        {-# ATP prove prf #-}
not-Bool bfalse = prf
  where postulate prf : Bool (not false)
        {-# ATP prove prf #-}

&&-list₂-t : ∀ {a b} → Bool a → Bool b → a && b ≡ true → a ≡ true ∧ b ≡ true
&&-list₂-t btrue btrue h = prf
  where postulate prf : true ≡ true ∧ true ≡ true
        {-# ATP prove prf #-}
&&-list₂-t btrue bfalse h = prf
  where postulate prf : true ≡ true ∧ false ≡ true
        {-# ATP prove prf #-}
&&-list₂-t bfalse btrue h = prf
  where postulate prf : false ≡ true ∧ true ≡ true
        {-# ATP prove prf #-}
&&-list₂-t bfalse bfalse h = prf
  where postulate prf : false ≡ true ∧ false ≡ true
        {-# ATP prove prf #-}

&&-list₂-t₁ : ∀ {a b} → Bool a → Bool b → a && b ≡ true → a ≡ true
&&-list₂-t₁ {a} Ba Bb h = prf
  where postulate prf : a ≡ true
        {-# ATP prove prf &&-list₂-t #-}

&&-list₂-t₂ : ∀ {a b} → Bool a → Bool b → a && b ≡ true → b ≡ true
&&-list₂-t₂ {b = b} Ba Bb h = prf
  where postulate prf : b ≡ true
        {-# ATP prove prf &&-list₂-t #-}

&&-list₄-t : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
             a && b && c && d ≡ true →
             a ≡ true ∧ b ≡ true ∧ c ≡ true ∧ d ≡ true
&&-list₄-t btrue btrue btrue btrue h = prf
  where postulate prf : true ≡ true ∧ true ≡ true ∧ true ≡ true ∧ true ≡ true
        {-# ATP prove prf #-}
&&-list₄-t btrue btrue btrue bfalse h = prf
  where postulate prf : true ≡ true ∧ true ≡ true ∧ true ≡ true ∧ false ≡ true
        {-# ATP prove prf #-}
&&-list₄-t {d = d} btrue btrue bfalse Bd h = prf
  where postulate prf : true ≡ true ∧ true ≡ true ∧ false ≡ true ∧ d ≡ true
        {-# ATP prove prf #-}
&&-list₄-t {c = c} {d} btrue bfalse Bc Bd h = prf
  where postulate prf : true ≡ true ∧ false ≡ true ∧ c ≡ true ∧ d ≡ true
        {-# ATP prove prf #-}
&&-list₄-t {b = b} {c} {d} bfalse Bb Bc Bd h = prf
  where postulate prf : false ≡ true ∧ b ≡ true ∧ c ≡ true ∧ d ≡ true
        {-# ATP prove prf #-}

&&-list₄-t₁ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → a ≡ true
&&-list₄-t₁ {a} Ba Bb Bc Bd h = prf
  where postulate prf : a ≡ true
        {-# ATP prove prf &&-list₄-t #-}

&&-list₄-t₂ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → b ≡ true
&&-list₄-t₂ {b = b} Ba Bb Bc Bd h = prf
  where postulate prf : b ≡ true
        {-# ATP prove prf &&-list₄-t #-}

&&-list₄-t₃ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → c ≡ true
&&-list₄-t₃ {c = c} Ba Bb Bc Bd h = prf
  where postulate prf : c ≡ true
        {-# ATP prove prf &&-list₄-t #-}

&&-list₄-t₄ : ∀ {a b c d} → Bool a → Bool b → Bool c → Bool d →
              a && b && c && d ≡ true → d ≡ true
&&-list₄-t₄ {d = d} Ba Bb Bc Bd h = prf
  where postulate prf : d ≡ true
        {-# ATP prove prf &&-list₄-t #-}

x≢not-x : ∀ {b} → Bool b → b ≢ not b
x≢not-x btrue h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}
x≢not-x bfalse h = prf
  where postulate prf : ⊥
        {-# ATP prove prf #-}

not-x≢x : ∀ {b} → Bool b → not b ≢ b
not-x≢x Bb h = prf
  where postulate prf : ⊥
        {-# ATP prove prf x≢not-x #-}

not-involutive : ∀ {b} → Bool b → not (not b) ≡ b
not-involutive btrue = prf
  where postulate prf : not (not true) ≡ true
        {-# ATP prove prf #-}
not-involutive bfalse = prf
  where postulate prf : not (not false) ≡ false
        {-# ATP prove prf #-}

------------------------------------------------------------------------------
-- Properties with inequalities

lt-Bool : ∀ {m n} → N m → N n → Bool (lt m n)
lt-Bool nzero nzero = prf
  where postulate prf : Bool (lt zero zero)
        {-# ATP prove prf #-}
lt-Bool nzero (nsucc {n} Nn) = prf
  where postulate prf : Bool (lt zero (succ₁ n))
        {-# ATP prove prf #-}
lt-Bool (nsucc {m} Nm) nzero = prf
  where postulate prf : Bool (lt (succ₁ m)  zero)
        {-# ATP prove prf #-}
lt-Bool (nsucc {m} Nm) (nsucc {n} Nn) = prf (lt-Bool Nm Nn)
  where postulate prf : Bool (lt m n) → Bool (lt (succ₁ m) (succ₁ n))
        {-# ATP prove prf #-}

le-Bool : ∀ {m n} → N m → N n → Bool (le m n)
le-Bool {n = n} nzero Nn = prf
  where postulate prf : Bool (le zero n)
        {-# ATP prove prf #-}
le-Bool (nsucc {m} Nm) nzero = prf
  where postulate prf : Bool (le (succ₁ m) zero)
        {-# ATP prove prf Sx≰0 #-}
le-Bool (nsucc {m} Nm) (nsucc {n} Nn) = prf (le-Bool Nm Nn)
  where postulate prf : Bool (le m n) → Bool (le (succ₁ m) (succ₁ n))
        {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommSemiring.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.SIP using (TypeWithStr)

open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Monoid

private
  variable
    ℓ ℓ' : Level

record IsCommSemiring {R : Type ℓ}
                  (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where

  field
    +IsCommMonoid  : IsCommMonoid 0r _+_
    ·IsCommMonoid  : IsCommMonoid 1r _·_
    ·LDist+        : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
    AnnihilL       : (x : R) → 0r · x ≡ 0r

  open IsCommMonoid +IsCommMonoid public
    renaming
      ( isSemigroup to +IsSemigroup
      ; isMonoid    to +IsMonoid)

  open IsCommMonoid ·IsCommMonoid public
    renaming
      ( isSemigroup to ·IsSemigroup
      ; isMonoid    to ·IsMonoid)
    hiding
      ( is-set ) -- We only want to export one proof of this

record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  field
    0r      : A
    1r      : A
    _+_     : A → A → A
    _·_     : A → A → A
    isCommSemiring  : IsCommSemiring 0r 1r _+_ _·_

  infixl 7 _·_
  infixl 6 _+_

  open IsCommSemiring isCommSemiring public

CommSemiring : ∀ ℓ → Type (ℓ-suc ℓ)
CommSemiring ℓ = TypeWithStr ℓ CommSemiringStr

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K #-}

open import Base
open import Homotopy.Pushout

module Homotopy.VanKampen {i} (d : pushout-diag i) where
open pushout-diag d

open import Homotopy.Truncation
open import Homotopy.PathTruncation
open import Homotopy.VanKampen.Guide

module _ (l : legend i C) where
  open legend l

  open import Homotopy.VanKampen.Code d l
  open import Homotopy.VanKampen.CodeToPath d l

  private
    refl⇒code : ∀ p → code p p
    refl⇒code = pushout-rec
      (λ p → code p p)
      (λ _ → ⟧a refl₀)
      (λ _ → ⟧b refl₀)
      (loc-fiber-rec l
        (λ c → transport (λ p → code p p) (glue c) (⟧a refl₀)
             ≡ ⟧b refl₀)
        ⦃ λ _ → b-code-b-is-set _ _ _ _ ⦄
        (λ n →
          transport (λ p → code p p) (glue $ loc n) (⟧a refl₀)
              ≡⟨ trans-diag code (glue $ loc n) $ ⟧a refl₀ ⟩
          transport (λ p → code p (right $ g $ loc n)) (glue $ loc n)
            (transport (a-code (f $ loc n)) (glue $ loc n) (⟧a refl₀))
              ≡⟨ ap (transport (λ p → code p (right $ g $ loc n)) (glue $ loc n))
                    $ trans-a-code-glue-loc n $ ⟧a refl₀ ⟩
          transport (λ p → code p (right $ g $ loc n)) (glue $ loc n) (aa⇒ab n (⟧a refl₀))
              ≡⟨ trans-glue-code-loc n {right $ g $ loc n} $ aa⇒ab n (⟧a refl₀) ⟩
          ab⇒bb n (aa⇒ab n (⟧a refl₀))
              ≡⟨ refl ⟩
          ⟧b refl₀ bb⟦ n ⟧a refl₀ ba⟦ n ⟧b refl₀
              ≡⟨ b-code-b-refl-refl _ _ ⟩∎
          ⟧b refl₀
              ∎))

  path⇒code : ∀ {p₁} {p₂} (q : p₁ ≡₀ p₂) → code p₁ p₂
  path⇒code {p₁} {p₂} = π₀-extend-nondep
    ⦃ code-is-set p₁ p₂ ⦄
    (λ q → transport (code p₁) q (refl⇒code p₁))

  private
    refl⇒code⇒path : ∀ p → code⇒path (refl⇒code p) ≡ refl₀ {a = p}
    refl⇒code⇒path = pushout-rec
      (λ p → code⇒path (refl⇒code p) ≡ refl₀)
      (λ _ → refl)
      (λ _ → refl)
      (λ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _)

    path′⇒code⇒path : ∀ {p₁ p₂} (q : p₁ ≡ p₂) → code⇒path (path⇒code $ proj q) ≡ proj q
    path′⇒code⇒path refl = refl⇒code⇒path _

  path⇒code⇒path : ∀ {p₁ p₂} (q : p₁ ≡₀ p₂) → code⇒path (path⇒code q) ≡ q
  path⇒code⇒path {p₁} {p₂} = π₀-extend
    ⦃ λ _ → ≡-is-set $ π₀-is-set (p₁ ≡ p₂) ⦄
    (path′⇒code⇒path {p₁} {p₂})

  private
    pgl : ∀ n → _≡₀_ {A = P} (left (f $ loc n)) (right (g $ loc n))
    pgl n = proj (glue $ loc n)

    p!gl : ∀ n → _≡₀_ {A = P} (right (g $ loc n)) (left (f $ loc n))
    p!gl n = proj (! (glue $ loc n))

    ap₀l : ∀ {a₁ a₂} → a₁ ≡₀ a₂ → _≡₀_ {A = P} (left a₁) (left a₂)
    ap₀l p = ap₀ left p

    ap₀r : ∀ {b₁ b₂} → b₁ ≡₀ b₂ → _≡₀_ {A = P} (right b₁) (right b₂)
    ap₀r p = ap₀ right p

  private
    path⇒code-concat₀ : ∀ {p₁ p₂ p₃} (q : p₁ ≡₀ p₂) (r : p₂ ≡ p₃)
      → path⇒code (q ∘₀ proj r) ≡ transport (code p₁) r (path⇒code q)
    path⇒code-concat₀ q refl = ap path⇒code $ refl₀-right-unit q

    module _ {a₁} where
      ap⇒path⇒ap-split :
          (∀ {a₂} (co : a-code-a a₁ a₂) → path⇒code (aa⇒path co) ≡ co)
        × (∀ {b₂} (co : a-code-b a₁ b₂) → path⇒code (ab⇒path co) ≡ co)
      ap⇒path⇒ap-split = a-code-rec a₁
        (λ {a₂} (co : a-code-a a₁ a₂) → path⇒code (aa⇒path co) ≡ co)
        ⦃ λ {a₂} _ → ≡-is-set $ a-code-a-is-set a₁ a₂ ⦄
        (λ {b₂} (co : a-code-b a₁ b₂) → path⇒code (ab⇒path co) ≡ co)
        ⦃ λ {b₂} _ → ≡-is-set $ a-code-b-is-set a₁ b₂ ⦄
        (λ {a₂} p → π₀-extend
          {P = λ p → path⇒code (aa⇒path $ ⟧a p) ≡ ⟧a p}
          ⦃ λ _ → ≡-is-set $ a-code-a-is-set a₁ a₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code (ap₀l p′)
              ≡⟨ refl ⟩
            transport (a-code a₁) (ap left p) (path⇒code $ refl₀ {a = left a₁})
              ≡⟨ trans-ap (a-code a₁) left p $ ⟧a refl₀ ⟩
            transport (a-code-a a₁) p (⟧a refl₀)
              ≡⟨ trans-a-code-a p refl₀ ⟩∎
            ⟧a proj p
              ∎) p)
        (λ {a₂} n {co} eq p → π₀-extend
          {P = λ p → path⇒code (aa⇒path $ co ab⟦ n ⟧a p) ≡ co ab⟦ n ⟧a p}
          ⦃ λ _ → ≡-is-set $ a-code-a-is-set a₁ a₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code ((ab⇒path co ∘₀ p!gl n) ∘₀ ap₀l p′)
                ≡⟨ path⇒code-concat₀ (ab⇒path co ∘₀ p!gl n) (ap left p) ⟩
            transport (a-code a₁) (ap left p) (path⇒code (ab⇒path co ∘₀ p!gl n))
                ≡⟨ trans-ap (a-code a₁) left p $ path⇒code $ ab⇒path co ∘₀ p!gl n ⟩
            transport (a-code-a a₁) p (path⇒code (ab⇒path co ∘₀ p!gl n))
                ≡⟨ ap (transport (a-code-a a₁) p)
                      $ path⇒code-concat₀ (ab⇒path co) (! (glue $ loc n)) ⟩
            transport (a-code-a a₁) p (transport (a-code a₁) (! (glue $ loc n))
              $ path⇒code $ ab⇒path co)
                ≡⟨ ap (transport (a-code-a a₁) p ◯ transport (a-code a₁) (! (glue $ loc n))) eq ⟩
            transport (a-code-a a₁) p (transport (a-code a₁) (! (glue $ loc n)) co)
                ≡⟨ ap (transport (a-code-a a₁) p) $ trans-a-code-!glue-loc n co ⟩
            transport (a-code-a a₁) p (co ab⟦ n ⟧a refl₀)
                ≡⟨ trans-a-code-ba p n co refl₀ ⟩∎
            co ab⟦ n ⟧a p′
                ∎) p)
        (λ {b₂} n {co} eq p → π₀-extend
          {P = λ p → path⇒code (ab⇒path $ co aa⟦ n ⟧b p) ≡ co aa⟦ n ⟧b p}
          ⦃ λ _ → ≡-is-set $ a-code-b-is-set a₁ b₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code ((aa⇒path co ∘₀ pgl n) ∘₀ ap₀r p′)
                ≡⟨ path⇒code-concat₀ (aa⇒path co ∘₀ pgl n) (ap right p) ⟩
            transport (a-code a₁) (ap right p) (path⇒code (aa⇒path co ∘₀ pgl n))
                ≡⟨ trans-ap (a-code a₁) right p $ path⇒code $ aa⇒path co ∘₀ pgl n ⟩
            transport (a-code-b a₁) p (path⇒code (aa⇒path co ∘₀ pgl n))
                ≡⟨ ap (transport (a-code-b a₁) p)
                      $ path⇒code-concat₀ (aa⇒path co) (glue $ loc n) ⟩
            transport (a-code-b a₁) p (transport (a-code a₁) (glue $ loc n)
              $ path⇒code $ aa⇒path co)
                ≡⟨ ap (transport (a-code-b a₁) p ◯ transport (a-code a₁) (glue $ loc n)) eq ⟩
            transport (a-code-b a₁) p (transport (a-code a₁) (glue $ loc n) co)
                ≡⟨ ap (transport (a-code-b a₁) p) $ trans-a-code-glue-loc n co ⟩
            transport (a-code-b a₁) p (co aa⟦ n ⟧b refl₀)
                ≡⟨ trans-a-code-ab p n co refl₀ ⟩∎
            co aa⟦ n ⟧b p′
                ∎) p)
        (λ _ _ → prop-has-all-paths (a-code-a-is-set a₁ _ _ _) _ _)
        (λ _ _ → prop-has-all-paths (a-code-b-is-set a₁ _ _ _) _ _)
        (λ _ _ _ _ → prop-has-all-paths (a-code-a-is-set a₁ _ _ _) _ _)

      ap⇒path⇒ap : ∀ {p₂} (co : a-code a₁ p₂) → path⇒code {left a₁} {p₂} (ap⇒path co) ≡ co
      ap⇒path⇒ap {p₂} = pushout-rec
        (λ x → ∀ (co : a-code a₁ x) → path⇒code {left a₁} {x} (ap⇒path co) ≡ co)
        (λ _ → π₁ ap⇒path⇒ap-split)
        (λ _ → π₂ ap⇒path⇒ap-split)
        (λ _ → funext λ _ → prop-has-all-paths (a-code-b-is-set a₁ _ _ _) _ _)
        p₂

    -- FIXME Duplicate code!
    -- Unless there's a way to handle type-conversion nicely
    -- (with definitional equality), I'd rather copy and paste.
    module _ {b₁} where
      bp⇒path⇒bp-split :
          (∀ {b₂} (co : b-code-b b₁ b₂) → path⇒code (bb⇒path co) ≡ co)
        × (∀ {a₂} (co : b-code-a b₁ a₂) → path⇒code (ba⇒path co) ≡ co)
      bp⇒path⇒bp-split = b-code-rec b₁
        (λ {b₂} (co : b-code-b b₁ b₂) → path⇒code (bb⇒path co) ≡ co)
        ⦃ λ {b₂} _ → ≡-is-set $ b-code-b-is-set b₁ b₂ ⦄
        (λ {a₂} (co : b-code-a b₁ a₂) → path⇒code (ba⇒path co) ≡ co)
        ⦃ λ {a₂} _ → ≡-is-set $ b-code-a-is-set b₁ a₂ ⦄
        (λ {b₂} p → π₀-extend
          {P = λ p → path⇒code (bb⇒path $ ⟧b p) ≡ ⟧b p}
          ⦃ λ _ → ≡-is-set $ b-code-b-is-set b₁ b₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code (ap₀r p′)
              ≡⟨ refl ⟩
            transport (b-code b₁) (ap right p) (path⇒code $ refl₀ {a = right b₁})
              ≡⟨ trans-ap (b-code b₁) right p $ ⟧b refl₀ ⟩
            transport (b-code-b b₁) p (⟧b refl₀)
              ≡⟨ trans-b-code-b p refl₀ ⟩∎
            ⟧b proj p
              ∎) p)
        (λ {b₂} n {co} eq p → π₀-extend
          {P = λ p → path⇒code (bb⇒path $ co ba⟦ n ⟧b p) ≡ co ba⟦ n ⟧b p}
          ⦃ λ _ → ≡-is-set $ b-code-b-is-set b₁ b₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code ((ba⇒path co ∘₀ pgl n) ∘₀ ap₀r p′)
                ≡⟨ path⇒code-concat₀ (ba⇒path co ∘₀ pgl n) (ap right p) ⟩
            transport (b-code b₁) (ap right p) (path⇒code (ba⇒path co ∘₀ pgl n))
                ≡⟨ trans-ap (b-code b₁) right p $ path⇒code $ ba⇒path co ∘₀ pgl n ⟩
            transport (b-code-b b₁) p (path⇒code (ba⇒path co ∘₀ pgl n))
                ≡⟨ ap (transport (b-code-b b₁) p)
                      $ path⇒code-concat₀ (ba⇒path co) (glue $ loc n) ⟩
            transport (b-code-b b₁) p (transport (b-code b₁) (glue $ loc n)
              $ path⇒code $ ba⇒path co)
                ≡⟨ ap (transport (b-code-b b₁) p ◯ transport (b-code b₁) (glue $ loc n)) eq ⟩
            transport (b-code-b b₁) p (transport (b-code b₁) (glue $ loc n) co)
                ≡⟨ ap (transport (b-code-b b₁) p) $ trans-b-code-glue-loc n co ⟩
            transport (b-code-b b₁) p (co ba⟦ n ⟧b refl₀)
                ≡⟨ trans-b-code-ab p n co refl₀ ⟩∎
            co ba⟦ n ⟧b p′
                ∎) p)
        (λ {a₂} n {co} eq p → π₀-extend
          {P = λ p → path⇒code (ba⇒path $ co bb⟦ n ⟧a p) ≡ co bb⟦ n ⟧a p}
          ⦃ λ _ → ≡-is-set $ b-code-a-is-set b₁ a₂ ⦄
          (λ p → let p′ = proj p in
            path⇒code ((bb⇒path co ∘₀ p!gl n) ∘₀ ap₀l p′)
                ≡⟨ path⇒code-concat₀ (bb⇒path co ∘₀ p!gl n) (ap left p) ⟩
            transport (b-code b₁) (ap left p) (path⇒code (bb⇒path co ∘₀ p!gl n))
                ≡⟨ trans-ap (b-code b₁) left p $ path⇒code $ bb⇒path co ∘₀ p!gl n ⟩
            transport (b-code-a b₁) p (path⇒code (bb⇒path co ∘₀ p!gl n))
                ≡⟨ ap (transport (b-code-a b₁) p)
                      $ path⇒code-concat₀ (bb⇒path co) (! (glue $ loc n)) ⟩
            transport (b-code-a b₁) p (transport (b-code b₁) (! (glue $ loc n))
              $ path⇒code $ bb⇒path co)
                ≡⟨ ap (transport (b-code-a b₁) p ◯ transport (b-code b₁) (! (glue $ loc n))) eq ⟩
            transport (b-code-a b₁) p (transport (b-code b₁) (! (glue $ loc n)) co)
                ≡⟨ ap (transport (b-code-a b₁) p) $ trans-b-code-!glue-loc n co ⟩
            transport (b-code-a b₁) p (co bb⟦ n ⟧a refl₀)
                ≡⟨ trans-b-code-ba p n co refl₀ ⟩∎
            co bb⟦ n ⟧a p′
                ∎) p)
        (λ _ _ → prop-has-all-paths (b-code-b-is-set b₁ _ _ _) _ _)
        (λ _ _ → prop-has-all-paths (b-code-a-is-set b₁ _ _ _) _ _)
        (λ _ _ _ _ → prop-has-all-paths (b-code-b-is-set b₁ _ _ _) _ _)

      bp⇒path⇒bp : ∀ {p₂} (co : b-code b₁ p₂) → path⇒code {right b₁} {p₂} (bp⇒path co) ≡ co
      bp⇒path⇒bp {p₂} = pushout-rec
        (λ x → ∀ (co : b-code b₁ x) → path⇒code {right b₁} {x} (bp⇒path co) ≡ co)
        (λ _ → π₂ bp⇒path⇒bp-split)
        (λ _ → π₁ bp⇒path⇒bp-split)
        (λ _ → funext λ _ → prop-has-all-paths (b-code-b-is-set b₁ _ _ _) _ _)
        p₂

  code⇒path⇒code : ∀ {p₁ p₂} (co : code p₁ p₂) → path⇒code {p₁} {p₂} (code⇒path co) ≡ co
  code⇒path⇒code {p₁} {p₂} = pushout-rec
    (λ p₁ → ∀ (co : code p₁ p₂) → path⇒code {p₁} {p₂} (code⇒path co) ≡ co)
    (λ a₁ → ap⇒path⇒ap {a₁} {p₂})
    (λ b₁ → bp⇒path⇒bp {b₁} {p₂})
    (λ c → funext λ co → prop-has-all-paths (b-code-is-set (g c) p₂ _ co) _ _)
    p₁

  van-kampen : ∀ {p₁ p₂} → (p₁ ≡₀ p₂) ≡ code p₁ p₂
  van-kampen {p₁} {p₂} =
    eq-to-path $ path⇒code {p₁} {p₂} ,
      iso-is-eq (path⇒code {p₁} {p₂}) (code⇒path {p₁} {p₂})
        (code⇒path⇒code {p₁} {p₂}) (path⇒code⇒path {p₁} {p₂})

module _ where
  open import Homotopy.VanKampen.Code d (id-legend C)

  naive-van-kampen : ∀ {p₁ p₂} → (p₁ ≡₀ p₂) ≡ code p₁ p₂
  naive-van-kampen = van-kampen (id-legend C)

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Inception | IA

type
  L : 0-ary
  P : 0-ary
  A : 0-ary

term
  rec : L  P  ->  A
  inc : L.A  P.A  ->  A

theory
  (S) p : P   a : P.A |> inc (l. rec (l, p[]), x. a[x]) = a[p[]]
  (E) a : L.A  |> k : L |- inc (l. a[l], x. rec(k, x)) = a[k]
  (W) m : A  a : P.A  |> inc (l. m[], x. a[x]) = m[]
  (A) p : (L,L).A  a : (L,P).A  b : P.A |>         inc (l. inc (k. p[l, k], x. a[l,x]), y. b[y])       = inc (k. inc(l. p[l,k], y.b[y]), x. inc(l. a[l,x], y.b[y]))
-}

module Inception.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Inception.Signature
open import Inception.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution IA:Syn
open import SOAS.Metatheory.SecondOrder.Equality IA:Syn

private
  variable
    α β γ τ : IAT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ IA) α Γ → (𝔐 ▷ IA) α Γ → Set where
  S : ⁅ P ⁆ ⁅ P ⊩ A ⁆̣ ▹   ∅   ⊢  inc (rec x₀ 𝔞) (𝔟⟨ x₀ ⟩) ≋ₐ 𝔟⟨ 𝔞 ⟩
  E : ⁅ L ⊩ A ⁆̣       ▹ ⌊ L ⌋ ⊢ inc (𝔞⟨ x₀ ⟩) (rec x₁ x₀) ≋ₐ 𝔞⟨ x₀ ⟩
  W : ⁅ A ⁆ ⁅ P ⊩ A ⁆̣ ▹   ∅   ⊢           inc 𝔞 (𝔟⟨ x₀ ⟩) ≋ₐ 𝔞
  A : ⁅ L · L ⊩ A ⁆ ⁅ L · P ⊩ A ⁆ ⁅ P ⊩ A ⁆̣ ▹ ∅
    ⊢ inc (inc (𝔞⟨ x₁ ◂ x₀ ⟩) (𝔟⟨ x₁ ◂ x₀ ⟩)) (𝔠⟨ x₀ ⟩)
   ≋ₐ inc (inc (𝔞⟨ x₀ ◂ x₁ ⟩) (𝔠⟨ x₀ ⟩)) (inc (𝔟⟨ x₀ ◂ x₁ ⟩) (𝔠⟨ x₀ ⟩))

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas